Soundness of Inprocessing in Clause Sharing SAT Solvers
作者： Norbert Manthey , Tobias Philipp , Christoph Wernhard
DOI: 10.1007/978-3-642-39071-5_4
关键词:
摘要: We present a formalism that models the computation of clause sharing portfolio solvers with inprocessing. The soundness these is not straightforward property since shared clauses can make formula unsatisfiable. Therefore, we develop characterizations simplification techniques and suggest various settings how inprocessing be combined. Our formalization most recent implemented systems indicate possibilities to improve these. A particular improvement novel way combine addition --- like blocked deletion elimination or variable elimination.
springer.com
christophwernhard.com 参考文章(48)
Davide Lanti, Norbert Manthey, Sharing Information in Parallel Search with Search Space Partitioning Lecture Notes in Computer Science. pp. 52- 58 ,(2013) , 10.1007/978-3-642-44973-4_6
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
Norbert Manthey, Marijn J. H. Heule, Armin Biere, Automated Reencoding of Boolean Formulas Hardware and Software: Verification and Testing. pp. 102- 117 ,(2013) , 10.1007/978-3-642-39611-3_14
Gilles Audemard, Laurent Simon, Predicting learnt clauses quality in modern SAT solvers international joint conference on artificial intelligence. pp. 399- 404 ,(2009)
Antti E. J. Hyvärinen, Norbert Manthey, Designing scalable parallel SAT solvers theory and applications of satisfiability testing. pp. 214- 227 ,(2012) , 10.1007/978-3-642-31612-8_17
Norbert Manthey, Coprocessor 2.0: a flexible CNF simplifier theory and applications of satisfiability testing. pp. 436- 441 ,(2012) , 10.1007/978-3-642-31612-8_34
Principles and Practice of Constraint Programming – CP 2010 Lecture Notes in Computer Science. ,vol. 6308, ,(2010) , 10.1007/978-3-642-15396-9
Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette, Revisiting clause exchange in parallel SAT solving theory and applications of satisfiability testing. ,vol. 7962, pp. 200- 213 ,(2012) , 10.1007/978-3-642-31612-8_16
Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, On freezing and reactivating learnt clauses theory and applications of satisfiability testing. pp. 188- 200 ,(2011) , 10.1007/978-3-642-21581-0_16
Antti E. J. Hyvärinen, Tommi Junttila, Ilkka Niemelä, Grid-based SAT solving with iterative partitioning and clause learning principles and practice of constraint programming. pp. 385- 399 ,(2011) , 10.1007/978-3-642-23786-7_30