Efficient Term-ITE Conversion for Satisfiability Modulo Theories

Autor:	Hyondeuk Kim, Fabio Somenzi, Hoonsang Jin
Rok vydání:	2009
Předmět:	Propositional variable Programming language Boolean circuit Atomic formula Term (logic) computer.software_genre Exponential function TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Satisfiability modulo theories Linear arithmetic Rewriting Arithmetic computer Mathematics
Zdroj:	Lecture Notes in Computer Science ISBN: 9783642027765 SAT
DOI:	10.1007/978-3-642-02777-2_20
Popis:	This paper describes how term-if-then-else (term-ITE ) is handled in Satisfiability Modulo Theories (SMT) and to decide Linear Arithmetic Logic (LA ) in particular. Term-ITEs allow one to conveniently express verification conditions; hence, they are very common in practice. However, the theory provers of SMT solvers are usually designed to work on conjunctions of literals; therefore, the input formulae are rewritten so as to eliminate term-ITEs. The challenge in rewriting is to avoid introducing too many new variables, while avoiding as often as possible the exponential explosion that is frequent when a naive approach is applied. We propose a solution that is based on cofactoring and theory propagation, which often produces orders-of-magnitude speedups in several SMT solvers for LA problems.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::5b60196d0e6fa616186fbebc5d6c9e61 https://doi.org/10.1007/978-3-642-02777-2_20 Zobrazit plný text záznamu