Automatically Improving SAT Encoding of Constraint Problems Through Common Subexpression Elimination in Savile Row
Automatically Improving SAT Encoding of Constraint Problems Through Common Subexpression Elimination in Savile Row
复制标题
通过 Savile Row 中的公共子表达式消除自动改进约束问题的 SAT 编码
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Ian Miguel
中科院分区：
文献类型：
--
作者：
Peter William Nightingale;Patrick Spracklen;Ian Miguel
命题可满足性SAT问题实例的形成对于有效求解至关重要。这激发了对预处理和处理中技术的研究，其中SAT实例的重构与求解交织在一起。预处理和内处理在扩展SAT求解器的范围方面非常有效，但是它们必须在问题的最低级别表示上操作，即原始SAT子句，其中更高级别的模式很难识别和/或识别成本很高。我们的方法不同：而不是直接重新表述SAT表示，我们应用自动重新表述到一个更高层次的表示原始问题的约束模型。公共子表达式消除CSE是一系列自动改进约束满足问题的公式化的技术，当使用传统的约束求解器时，这通常是非常有益的。在这项工作中，我们证明了CSE具有类似的好处时，重新制定的约束模型被编码为SAT和解决使用一个国家的最先进的SAT求解器。在某些情况下，我们观察到速度提高了100倍以上。
The formulation of a Propositional Satisfiability SAT problem instance is vital to efficient solving. This has motivated research on preprocessing, and inprocessing techniques where reformulation of a SAT instance is interleaved with solving. Preprocessing and inprocessing are highly effective in extending the reach of SAT solvers, however they necessarily operate on the lowest level representation of the problem, the raw SAT clauses, where higher-level patterns are difficult and/or costly to identify. Our approach is different: rather than reformulate the SAT representation directly, we apply automated reformulations to a higher level representation a constraint model of the original problem. Common Subexpression Elimination CSE is a family of techniques to improve automatically the formulation of constraint satisfaction problems, which are often highly beneficial when using a conventional constraint solver. In this work we demonstrate that CSE has similar benefits when the reformulated constraint model is encoded to SAT and solved using a state-of-the-art SAT solver. In some cases we observe speed improvements of over 100 times.
DOI：
--
发表时间：
2010
期刊：
--
影响因子：
--
作者：
Rendl Andrea
通讯作者：
Rendl Andrea