Tomas Balyo, Andreas Fröhlich, Marijn Heule, Armin Biere,
"Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)"
: Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Serie Lecture Notes in Computer Science (LNCS), Vol. 8561, Springer, Seite(n) 317-332, 2014
Original Titel:
Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14)
Original Kurzfassung:
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.
Forschungs-