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

• Type: Journal
• Year: 2010
• Where: MEMOCODE
• Authors: Roberto Bruttomesso, Edgar Pek, Natasha Sharygina
• Keywords: Consistency Check Procedure, Formal Methods, MEMOCODE 2010, Satisfiability Modulo Theories, Theory Propagation