Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row
| Autor: | Peter Nightingale, Patrick Spracklen, Ian Miguel |
|---|---|
| Přispěvatelé: | Pesant, Gilles, EPSRC, University of St Andrews. School of Computer Science, University of St Andrews. Centre for Interdisciplinary Research in Computational Algebra |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
Constraint (information theory)
QA75 Theoretical computer science Negation normal form Computer science Encoding (memory) QA75 Electronic computers. Computer science Common subexpression elimination 3rd-DAS Boolean satisfiability problem Representation (mathematics) Satisfiability Constraint satisfaction problem |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319232188 CP |
| Popis: | 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. Postprint |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|