Sciweavers

Share
MEMOCODE
2010
IEEE

A flexible schema for generating explanations in lazy theory propagation

8 years 3 months ago
A flexible schema for generating explanations in lazy theory propagation
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 SATSolver. 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).
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where MEMOCODE
Authors Roberto Bruttomesso, Edgar Pek, Natasha Sharygina
Comments (0)
books