Non-Clausal Satisfiability Modulo Theories

This thesis presents NC(T), an extension of the DPLL(T) scheme [16, 29] for decision procedures for quantifier-free first-order logics. In DPLL(T), a general Boolean DPLL engine is instantiated with a theory solver for the theory T. The DPLL engine is responsible for computing Boolean implications and detecting Boolean conflicts, while the theory solver detects implications and conflicts in T, and the communication between the two parts is done through a standardized interface. The Boolean reasoning is done on a set of constraints represented as clauses, meaning that formulas have to be converted to conjunctive normal form before they can be processed. The process results in the addition of variables and a general loss of structure. NC(T) remove this constraint by extending the Boolean engine to support the detection of implications and conflicts on non–clausal constraints, using techniques working on graphical representations of formulas in negation normal form first described in [19, 21]. Conversion to negation normal form preserves the size and structure of the input formula and does not introduce new variables. The above scheme NC(T) has been implemented as a tool called fstp, where the theory T under consideration is the quantifier–free theory of uninterpreted function and predicate symbols with equality. We describe our implementation and give early experimental results.