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

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2014

Kód důvěrnosti údajů

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

Název statě ve sborníku

Lecture Notes in Computer Science

ISBN

978-3-319-09284-3

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

16

Strana od-do

317-332

Název nakladatele

SPRINGER-VERLAG BERLIN

Místo vydání

BERLIN

Místo konání akce

Vienna, Austria

Datum konání akce

14. 7. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000345595300024