# Topics in Model-Based Reasoning

## Towards Integration of Proving and Solving

A 3h lecture within an Advanced Seminar in Artificial Intelligence and Robotics at the Università degli Studi di Roma ``La Sapienza''.

Abstract
Proofs and models are the mainstay of automated reasoning. Traditionally, proofs have taken center stage, because in first-order logic theorem proving is semi-decidable, and model building is not. The growth of algorithmic reasoning and of its applications to software has changed the balance, because if satisfiability is decidable, symmetry is restored, and models are useful for applications and intuitive for users. This lecture covers both classical and recent topics in model-based reasoning, where models take center stage as much as proofs.

Introduction
Many approaches in AI revolve around proofs and models. A proof is a formal argument that a claim holds. A model is a formal description of a state of a system. Proofs and models are related: proving by refutation means showing that the negation of the claim has no model, so that the claim is valid; if the proofs fails, a model of the negation of the claim is a counter-example. Solving a set of constraints means finding a satisfying assignment for the variables, and such an assignment is a model; if the search for a model fails, there is a proof. From a proving perspective, a proof means success and its failure gives a model; from a solving perspective, a model means success and its absence gives a proof.
The choice of perspective depends on decidability, which is inversely related to expressivity. In first-order logic, theorem proving is semi-decidable, and model finding is not; the proving perspective prevails, and reasoners are provers. In propositional logic, and decidable first-order theories, decidability restores the symmetry; the solving perspective prevails, and reasoners are solvers.

Motivation and Aim
While the distinction between semi-decidable and decidable, or, equivalently, between infinite and finite search space, separates proving and solving, applications unite them. It is disappointing to have a theorem prover that finds proofs in first-order logic, but cannot solve problems in arithmetic, or having an SMT-solver that solves problems in arithmetic or bitvectors, but cannot handle quantifiers, that are ubiquitous, for instance, in program verification. Thus, the goal is to advance the integration of proving and solving.

A double challenge
Prover and solver operate differently. In first-order theorem proving model representation is difficult; there are models with infinite domain; models are not unique; problems are stated axiomatically as a set of clauses; there is no intended model; the reasoner performs inferences to get a contradiction; models or their non-existence remain implicit. In SAT and SMT solving a model is represented finitely by an assignment of values to variables; an interpretation is intended; the theory is defined by a set of models, rather than by a set of axioms; the reasoner searches for a model, by maintaining a candidate partial model and trying to complete it. How can we integrate first-order theorem prover and SMT-solver? How can we integrate inference and search so that they guide each other?

Class Outline

• I part: A classic from the literature: the Davis-Putnam-Logemann-Loveland procedure with conflict driven clause learning (DPLL-CDCL), or how the integration of search and inference in propositional logic brought Boolean satisfiability from theoretical hardness to practical success.
• II part: A recent research accomplishment: the DPLL(Γ+T) method, or the tight integration of SMT-solver and first-order theorem prover.
• III part: Discussion of current trends in the field: integration of search and inference in first-order theories.

References:

• For the I part:
• João P. Marques-Silva and Karem A. Sakallah. GRASP: A new search algorithm for satisfiability. Proceedings of ICCAD 1996, 220-227, 1997.
• Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik. Chaff: Engineering an efficient SAT solver. Proceedings of DAC-39, 530-535, 2001.
• Lintao Zhang and Sharad Malik. The quest for efficient boolean satisfiability solvers. Proceedings of CADE-18, LNAI 2392:295-313, Springer 2002.
• Sharad Malik and Lintao Zhang. Boolean satisfiability from theoretical hardness to practical success. Communications of the ACM, 52(8):76-82, 2009.
• For the II part:
• For the III part:
• Leonardo de Moura and Dejan Jovanović. A model-constructing satisfiability calculus. Proceedings of VMCAI-14, LNCS 7737:1-12, Springer, 2013.
• Dejan Jovanović, Clark Barrett and Leonardo de Moura. The design and implementation of the model-constructing satisfiability calculus. Procedings of FMCAD-13, ACM and IEEE, 2013. 