On Simplification of Formulas with Unconstrained Variables and
Quantifiers

D 2017

On Simplification of Formulas with Unconstrained Variables and Quantifiers

JONÁŠ, Martin a Jan STREJČEK

Základní údaje

Originální název

On Simplification of Formulas with Unconstrained Variables and Quantifiers

Autoři

JONÁŠ, Martin (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Cham (Switzerland), Theory and Applications of Satisfiability Testing – SAT 2017, od s. 364-379, 16 s. 2017

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/17:00095125

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-66262-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-66263-3_23

UT WoS

000455337600023

Klíčová slova anglicky

SMT solving; formula simplifications; bit-vectors

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 14. 5. 2020 15:12, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

MUNI/A/0897/2016, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0992/2016, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

JONÁŠ, Martin a Jan STREJČEK. On Simplification of Formulas with Unconstrained Variables and Quantifiers. In Serge Gaspers, Toby Walsh. Theory and Applications of Satisfiability Testing – SAT 2017. Cham (Switzerland): Springer, 2017, s. 364-379. ISBN 978-3-319-66262-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-66263-3_23.

@inproceedings{1394152,
   author = {Jonáš, Martin and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Theory and Applications of Satisfiability Testing – SAT 2017},
   doi = {http://dx.doi.org/10.1007/978-3-319-66263-3_23},
   editor = {Serge Gaspers, Toby Walsh},
   keywords = {SMT solving; formula simplifications; bit-vectors},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-319-66262-6},
   pages = {364-379},
   publisher = {Springer},
   title = {On Simplification of Formulas with Unconstrained Variables and Quantifiers},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-319-66263-3_23},
   year = {2017}
}

TY  - JOUR
ID  - 1394152
AU  - Jonáš, Martin - Strejček, Jan
PY  - 2017
TI  - On Simplification of Formulas with Unconstrained Variables and Quantifiers
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783319662626
KW  - SMT solving
KW  - formula simplifications
KW  - bit-vectors
UR  - https://link.springer.com/chapter/10.1007%2F978-3-319-66263-3_23
N2  - 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.
ER  -

JONÁŠ, Martin a Jan STREJČEK. On Simplification of Formulas with Unconstrained Variables and Quantifiers. In Serge Gaspers, Toby Walsh. \textit{Theory and Applications of Satisfiability Testing – SAT 2017}. Cham (Switzerland): Springer, 2017, s.~364-379. ISBN~978-3-319-66262-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-66263-3\_{}23.

Podrobný výpis o publikaci