Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F13%3A10144125" target="_blank" >RIV/00216208:11320/13:10144125 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-319-00948-3_15" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-319-00948-3_15</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-00948-3_15" target="_blank" >10.1007/978-3-319-00948-3_15</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas

Popis výsledku v původním jazyce

An SMT-solving procedure can be implemented by using a SAT solver to find a satisfying assignment of the propositional skeleton of the predicate formula and then deciding the feasibility of the assignment using a particular decision procedure. The complexity of the decision procedure depends on the size of the assignment. In case that the runtime of the solving is dominated by the decision procedure it is convenient to find short satisfying assignments in the SAT solving phase. Unfortunately most of themodern state-of-the-art SAT solvers always output a complete assignment of variables for satisfiable formulas even if they can be satisfied by assigning truth values to only a fraction of the variables. In this paper,we first describe an application inthe code performance modeling domain, which requires SMT-solving with a costly decision procedure. Then we focus on the problem of finding minimum-size satisfying partial truth assignments. We describe and experimentally evaluate several

Název v anglickém jazyce

Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas

Popis výsledku anglicky

An SMT-solving procedure can be implemented by using a SAT solver to find a satisfying assignment of the propositional skeleton of the predicate formula and then deciding the feasibility of the assignment using a particular decision procedure. The complexity of the decision procedure depends on the size of the assignment. In case that the runtime of the solving is dominated by the decision procedure it is convenient to find short satisfying assignments in the SAT solving phase. Unfortunately most of themodern state-of-the-art SAT solvers always output a complete assignment of variables for satisfiable formulas even if they can be satisfied by assigning truth values to only a fraction of the variables. In this paper,we first describe an application inthe code performance modeling domain, which requires SMT-solving with a costly decision procedure. Then we focus on the problem of finding minimum-size satisfying partial truth assignments. We describe and experimentally evaluate several

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GCP202%2F10%2FJ042" target="_blank" >GCP202/10/J042: Vyhodnocování kvalitativních vlivů rozhodnutí z fáze softwarového návrhu pomocí modelování</a><br>

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2013

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

Studies in Computational Intelligence

ISBN

978-3-319-00947-6

ISSN

1860-949X

e-ISSN

—

Počet stran výsledku

16

Strana od-do

231-246

Název nakladatele

Springer International Publishing

Místo vydání

Switzerland

Místo konání akce

Prague, Czech Republic

Datum konání akce

7. 8. 2013

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

WRD - Celosvětová akce

Kód UT WoS článku

—