Blocked clause elimination is a powerful technique in SAT solving. In recent work, it has been shown that it is possible to decompose any propositional formula into two subsets (blocked sets) such that both can be solved by blocked clause elimination. We extend this work in several ways. First, we prove new theoretical properties of blocked sets. We then present additional and improved ways to efficiently solve blocked sets. Further, we propose novel decomposition algorithms for faster decomposition or which produce blocked sets with desirable attributes. We use decompositions to reencode CNF formulas and to obtain circuits, such as AIGs, which can then be simplified by algorithms from circuit synthesis and encoded back to CNF. Our experiments demonstrate that these techniques can increase the performance of the SAT solver Lingeling on hard to solve application benchmarks. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Balyo, T., Fröhlich, A., Heule, M. J. H., & Biere, A. (2014). Everything you always wanted to know about blocked sets (but were afraid to ask). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8561 LNCS, pp. 317–332). Springer Verlag. https://doi.org/10.1007/978-3-319-09284-3_24
Mendeley helps you to discover research relevant for your work.