最近收集了部分文献中实验设计如下：
|
1. 文献：Community Structure in Industrial SAT Instances A. 段落：第7节第4段后半段。讲解了一个实验，很有意思。 笔记：（1）关于SAT结论对应于可能有多个不同的赋值序列。特别是：Notice that this experiment is equivalent to removing all activitycounters used by the heuristic after timep t, and this may dramatically worsen the perfor-mance of the solver when the formula is satisfiable. （2）结论为UNSAT的样例，中途保留学习子句集而去掉过程累计的信息后重新求解，不影响整体求解时间。这说明UNSAT对过程量的依赖性很低，学习子句集的重要性比较突出。
B. 段落：第7节第4段后半段。讲解了第二个实验，也很有意思,并成为算法3，作为该文章的核心技术。 （1）Notice that the algorithm imposes a very strong condition, which is solving all subformulas between two connected communities and keepingalllearned clauses foundin this process. Notice that a solver not aware of thecommunity structure may remove them, unless, as we do, these clauses are added in apreprocessing step as original clauses, so the solver is forced to keep them （2）This could be further refined. 在子句中加入社区的数量作为决定子句删除的试探法，而不是在预处理中使用它，我们推测改进甚至会比我们在这个实验中观察到的更大。 （3）此外，这一预处理步骤可以在搜索过程中以内部处理方法的方式进行启发式应用.
|
|
| 2. 实验设计：已经求出结果的情况下，保留最后单元子句、决策序列、充当reason子句的所有学习子句。交给不同的求解器评价其某项策略的优劣。 | |
标签：Notice,solver,研究,求解,实验设计,子句,clauses From： https://www.cnblogs.com/yuweng1689/p/18071278