基于社区的3- SAT公式和预定义的解决方案
Community-based 3-SAT Formulas with a Predefined Solution
摘要：
对于SAT求解器的测试和开发来说，使用预定义的解决方案生成精心制作的SAT公式是至关重要的，因为现实世界中的许多SAT公式都有解决方案。虽然已经提出了一些生成算法来生成具有预定义解的SAT公式，但是没有考虑SAT公式的社区结构。我们提出了一个3-SAT公式生成算法，不仅保证存在一个预定义的解决方案，但也同时考虑社区结构和子句分布。所提出的3-SAT公式生成算法通过控制（1）其变量具有共同社区的子句的数量（我们称之为社区内子句）和（2）仅属于一个社区的变量的数量（我们称之为社区内变量）来控制社区结构的质量。为了研究社区结构和子句分布对SAT公式硬度的综合影响，我们测量了两个求解器，gluHack（领先的CDCL求解器）和CPSparrow（领先的SLS求解器），在不同的参数设置组下生成的SAT公式的求解运行时间。通过大量的实验，我们得到了一些值得注意的结果：（1）对于CPSparrow，社团结构对SAT公式的硬度影响很小，但对于gluHack，社团结构对SAT公式的硬度影响很大。(2)只有当SAT公式中的真文字在预定义解方面的比例为0.5时，SAT公式对于gluHack是难以求解的;当该比例低于0.5时，SAT公式对于CPSparrow是难以求解的。(3)当子句数与变量数之比约为4.25时，SAT公式对于gluHack和CPSparrow都难以求解。
英文摘要：
It is crucial to generate crafted SAT formulas with predefined solutions for the testing and development of SAT solvers since many SAT formulas from real-world applications have solutions. Although some generating algorithms have been proposed to generate SAT formulas with predefined solutions, community structures of SAT formulas are not considered. We propose a 3-SAT formula generating algorithm that not only guarantees the existence of a predefined solution, but also simultaneously considers community structures and clause distributions. The proposed 3-SAT formula generating algorithm controls the quality of community structures through controlling (1) the number of clauses whose variables have a common community, which we call intra-community clauses, and (2) the number of variables that only belong to one community, which we call intra-community variables. To study the combined effect of community structures and clause distributions on the hardness of SAT formulas, we measure solving runtimes of two solvers, gluHack (a leading CDCL solver) and CPSparrow (a leading SLS solver), on the generated SAT formulas under different groups of parameter settings. Through extensive experiments, we obtain some noteworthy observations on the SAT formulas generated by the proposed algorithm: (1) The community structure has little or no effects on the hardness of SAT formulas with regard to CPSparrow but a strong effect with regard to gluHack. (2) Only when the proportion of true literals in a SAT formula in terms of the predefined solution is 0.5, SAT formulas are hard-to-solve with regard to gluHack; when this proportion is below 0.5, SAT formulas are hard-to-solve with regard to CPSparrow. (3) When the ratio of the number of clauses to that of variables is around 4.25, the SAT formulas are hard-to-solve with regard to both gluHack and CPSparrow.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
