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. © 2013 Springer-Verlag.
CITATION STYLE
Manthey, N., Philipp, T., & Wernhard, C. (2013). Soundness of inprocessing in clause sharing SAT solvers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7962 LNCS, pp. 22–39). https://doi.org/10.1007/978-3-642-39071-5_4
Mendeley helps you to discover research relevant for your work.