Model-Driven Decision Procedures for Arithmetic

Summary form only given, as follows. Considering the theoretical hardness of SAT, the astonishing adeptness of SAT solvers when attacking practical problems has changed the way we perceive the limits of algorithmic reasoning. Modern SAT solvers are based on the idea of conflict driven clause learning (CDCL). The CDCL algorithm is a combination of an explicit backtracking search for a satisfying assignment complemented with a deduction system based on Boolean resolution. In this combination, the worst-case complexity of both components is circumvented by the components guiding and focusing each other. In this talk, we describe new procedures for nonlinear real arithmetic and linear integer arithmetic based on the CDCL algorithm. These procedures perform a backtracking search for a model, where the backtracking is powered by a novel conflict resolution procedure. Our approach takes advantage of the fact that each conflict encountered during the search is based on the current assignment and generally involves only a few constraints, a conflicting core. When in conflict, we project only the constraints from the conflicting core and explain the conflict in terms of the current model. The conflict resolution provides the usual benefits of a CDCL-style search engine, such as non-chronological backtracking and the ability to ignore irrelevant parts of the search space. The procedures described in the talk are instances of the model-constructing satisfiability calculus proposed by the authors.