Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F14%3A10285802" target="_blank" >RIV/00216208:11320/14:10285802 - isvavai.cz</a>
Result on the web
<a href="http://link.springer.com/chapter/10.1007/978-3-319-09284-3_24" target="_blank" >http://link.springer.com/chapter/10.1007/978-3-319-09284-3_24</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-09284-3_24" target="_blank" >10.1007/978-3-319-09284-3_24</a>

Result language
angličtina
Original language name
Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)
Original language description
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. Weextend 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 orwhich 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.
Czech name
—
Czech description
—

Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)