Shatter: efficient symmetry-breaking for Boolean satisfiability
Shatter: efficient symmetry-breaking for Boolean satisfiability
复制标题
Shatter：高效对称性破缺，实现布尔可满足性
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
K. Sakallah
中科院分区：
文献类型：
--
作者：
F. Aloul;I. Markov;K. Sakallah
根据E. Goldberg等人（2002）的说法，布尔可满足性（SAT）求解器在过去几年中在性能和可扩展性方面经历了巨大的改进，现在已常规用于各种EDA应用程序。然而，根据E. Goldberg等人（2002）的研究，在2002年SAT竞赛（http://www.satlive.org/SATCompetition/submittedbenchs.html）中，许多实际的SAT问题仍然难以解决，即使是最好的SAT解决方案也难以解决。最近的研究指出，布尔搜索空间的对称性往往是罪魁祸首。J. Crawford等人（1996）介绍了检测和打破这种对称性的理论框架。该框架随后被扩展、改进，并在F. Aloul等人（2002）的研究中通过经验证明对大量基准类产生了显著的加速。通过在合取范式（CNF）的SAT实例中添加适当的对称性破坏谓词（sbp）来打破搜索空间中的对称性。sbp充当过滤器，将搜索限制在空间的非对称区域，而不影响CNF公式的可满足性，从而对搜索空间进行精简。为了使对称破缺在实践中有效，生成和操作sbp的计算开销必须显著小于它们由于搜索空间修剪而节省的运行时间。在本文中，我们提出了几个新的sbp结构，改进了以前的工作。具体来说，我们给出了一个线性大小的CNF公式，该公式为单个排列选择词序（以及其他）。我们还展示了如何利用排列的稀疏性来简化该公式。我们针对早期的结构测试了这些改进，并表明它们产生更小的snp，并在许多基准测试中减少了运行时间。
Boolean satisfiability (SAT) solvers have experienced dramatic improvements in their performance and scalability over the last several years according to E. Goldberg et al. (2002) and are now routinely used in diverse EDA applications. Nevertheless, a number of practical SAT instances remain difficult to solve in SAT 2002 Competition (http://www.satlive.org/SATCompetition/submittedbenchs.html) and continue to defy even the best available SAT solvers according to E. Goldberg et al. (2002). Recent work pointed out that symmetries in the Boolean search space are often to blame. A theoretical framework for detecting and breaking such symmetries was introduced in J. Crawford et al. (1996). This framework was subsequently extended, refined, and empirically shown to yield significant speed-ups for a large number of benchmark classes in F. Aloul et al. (2002). Symmetries in the search space are broken by adding appropriate symmetry-breaking predicates (SBPs) to a SAT instance in conjunctive normal form (CNF). The SBPs prune the search space by acting as a filter that confines the search to nonsymmetric regions of the space without affecting the satisfiability of the CNF formula. For symmetry breaking to be effective in practice, the computational overhead of generating and manipulating the SBPs must be significantly less than the run time savings they yield due to search space pruning. In this paper, we present several new constructions of SBPs that improve on previous work. Specifically, we give a linear-sized CNF formula that selects lex-leaders (among others) for single permutations. We also show how that formula can be simplified by taking advantage of the sparsity of permutations. We test these improvements against earlier constructions and show that they yield smaller SNPs and lead to run time reductions on many benchmarks.