On Simplification of Formulas with Unconstrained Variables and Quantifiers
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F17%3A00095125" target="_blank" >RIV/00216224:14330/17:00095125 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-319-66263-3_23" target="_blank" >http://dx.doi.org/10.1007/978-3-319-66263-3_23</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-66263-3_23" target="_blank" >10.1007/978-3-319-66263-3_23</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
On Simplification of Formulas with Unconstrained Variables and Quantifiers
Popis výsledku v původním jazyce
Preprocessing of the input formula is an essential part of all modern smt solvers. An important preprocessing step is formula simplification. This paper elaborates on simplification of quantifier-free formulas containing unconstrained terms, i.e. terms that can have arbitrary values independently on the rest of the formula. We extend the idea in two directions. First, we introduce partially constrained terms and show some simplification rules employing this notion. Second, we show that unconstrained terms can be used also for simplification of formulas with quantifiers. Moreover, both these extensions can be merged in order to simplify partially constrained terms in formulas with quantifiers. We experimentally evaluate the proposed simplifications on formulas in the bit-vector theory.
Název v anglickém jazyce
On Simplification of Formulas with Unconstrained Variables and Quantifiers
Popis výsledku anglicky
Preprocessing of the input formula is an essential part of all modern smt solvers. An important preprocessing step is formula simplification. This paper elaborates on simplification of quantifier-free formulas containing unconstrained terms, i.e. terms that can have arbitrary values independently on the rest of the formula. We extend the idea in two directions. First, we introduce partially constrained terms and show some simplification rules employing this notion. Second, we show that unconstrained terms can be used also for simplification of formulas with quantifiers. Moreover, both these extensions can be merged in order to simplify partially constrained terms in formulas with quantifiers. We experimentally evaluate the proposed simplifications on formulas in the bit-vector theory.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2017
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ů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Theory and Applications of Satisfiability Testing – SAT 2017
ISBN
9783319662626
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
16
Strana od-do
364-379
Název nakladatele
Springer
Místo vydání
Cham (Switzerland)
Místo konání akce
Melbourne
Datum konání akce
1. 1. 2017
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—