DocumentCode :
1835749
Title :
A flexible schema for generating explanations in lazy theory propagation
Author :
Bruttomesso, Roberto ; Pek, Edgar ; Sharygina, Natasha
Author_Institution :
Univ. della Svizzera Italiana, Lugano, Switzerland
fYear :
2010
fDate :
26-28 July 2010
Firstpage :
41
Lastpage :
48
Abstract :
Theory propagation in Satisfiability Modulo Theories is crucial for the solver´s performance. It is important, however, to pay particular care to the amount of deductions to perform. The risk is in fact to clog the SAT-Solver with too many (and potentially useless clauses). In this paper we review some techniques for generating and communicating clauses to the SAT-Solver. In addition we propose a generic and flexible schema for theory propagation in which explanations for entailed facts are generated by re-using the consistency check procedure that is normally available in a theory solver. We argue that our schema can simplify the design of a theory solver, and allow a flexible form of theory propagation even for inherently hard theories (such as bit-vectors).
Keywords :
computability; SAT-solver; consistency check procedure; lazy theory propagation; satisfiability modulo theories; theory solver; Barium; Benchmark testing; Book reviews; Cotton; Databases; Radio access networks; Semantics;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Formal Methods and Models for Codesign (MEMOCODE), 2010 8th IEEE/ACM International Conference on
Conference_Location :
Grenoble
Print_ISBN :
978-1-4244-7885-9
Electronic_ISBN :
978-1-4244-7886-6
Type :
conf
DOI :
10.1109/MEMCOD.2010.5558625
Filename :
5558625
Link To Document :
بازگشت