zbMATH — the first resource for mathematics

Soundness of inprocessing in clause sharing SAT solvers. (English) Zbl 1390.68582
J√§rvisalo, Matti (ed.) et al., Theory and applications of satisfiability testing – SAT 2013. 16th international conference, Helsinki, Finland, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39070-8/pbk). Lecture Notes in Computer Science 7962, 22-39 (2013).
Summary: We present a formalism that models the computation of clause sharing portfolio solvers with inprocessing. The soundness of these solvers is not a straightforward property since shared clauses can make a formula unsatisfiable. Therefore, we develop characterizations of simplification techniques and suggest various settings how clause sharing and inprocessing can be combined. Our formalization models most of the recent implemented portfolio systems and we indicate possibilities to improve these. A particular improvement is a novel way to combine clause addition techniques – like blocked clause addition – with clause deletion techniques – like blocked clause elimination or variable elimination.
For the entire collection see [Zbl 1268.68023].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI