Encoding Linear constraints with implication chains to CNF
作者： Ignasi Abío , Valentin Mayer-Eichberger , Peter J. Stuckey
DOI: 10.1007/978-3-319-23219-5_1
关键词:
摘要: Linear constraints are the most common occurring in combinatorial problems. For some problems which combine linear with highly constraints, best solving method is translation to SAT. Translation of a single constraint SAT well studied problem, particularly for cardinality and pseudo-Boolean constraints. In this paper we describe how can improve encodings by taking into account implication chains problem. The resulting smaller propagate more strongly than separate encodings. We illustrate benchmarks where encoding improves performance.
springer.com
sci-hub.st 参考文章(17)
Marijn J. H. Heule, Matti Järvisalo, Armin Biere, Efficient CNF simplification based on binary implication graphs theory and applications of satisfiability testing. pp. 201- 215 ,(2011) , 10.1007/978-3-642-21581-0_17
Bruno Dutertre, Leonardo de Moura, The YICES SMT Solver ,(2006)
Ignasi Abío Roig, Solving hard industrial combinatorial problems with SAT TDX (Tesis Doctorals en Xarxa). ,(2013)
Ignasi Abío, Peter J. Stuckey, Encoding Linear Constraints into SAT principles and practice of constraint programming. pp. 75- 91 ,(2014) , 10.1007/978-3-319-10428-7_9
Olivier Bailleux, Yacine Boufkhad, Olivier Roussel, New Encodings of Pseudo-Boolean Constraints into CNF theory and applications of satisfiability testing. pp. 181- 194 ,(2009) , 10.1007/978-3-642-02777-2_19
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints principles and practice of constraint programming. pp. 80- 96 ,(2013) , 10.1007/978-3-642-40627-0_9
Hans van Maaren, Marijn Heule, Toby Walsh, Armin Biere, Handbook of satisfiability IOS Press. ,(2009)
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio, The Barcelogic SMT Solver computer aided verification. pp. 294- 298 ,(2008) , 10.1007/978-3-540-70545-1_27
Niklas Eén, Armin Biere, Effective Preprocessing in SAT Through Variable and Clause Elimination Theory and Applications of Satisfiability Testing. ,vol. 3569, pp. 61- 75 ,(2005) , 10.1007/11499107_5