On Simplification of Formulas with Unconstrained Variables and Quantifiers

Result code in 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>

Result on the web

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

Result language

angličtina

Original language name

On Simplification of Formulas with Unconstrained Variables and Quantifiers

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>

Continuities

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

Publication year

2017

Confidentiality

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

Article name in the collection

Theory and Applications of Satisfiability Testing – SAT 2017

ISBN

9783319662626

ISSN

0302-9743

e-ISSN

—

Number of pages

16

Pages from-to

364-379

Publisher name

Springer

Place of publication

Cham (Switzerland)

Event location

Melbourne

Event date

Jan 1, 2017

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—