Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas
Original language description
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
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GCP202%2F10%2FJ042" target="_blank" >GCP202/10/J042: Model-Driven Evaluation of Design Decision Impacts in Software Engineering</a><br>
Continuities
S - Specificky vyzkum na vysokych skolach
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Studies in Computational Intelligence
ISBN
978-3-319-00947-6
ISSN
1860-949X
e-ISSN
—
Number of pages
16
Pages from-to
231-246
Publisher name
Springer International Publishing
Place of publication
Switzerland
Event location
Prague, Czech Republic
Event date
Aug 7, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—