**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:
- Maria Paola Bonacina, Christopher A. Lynch and Leonardo de Moura.
On deciding satisfiability by theorem proving with speculative inferences.
*Journal of Automated Reasoning*, 47(2):161-189, August 2011; DOI: 10.1007/s10817-010-9213-y.

- Maria Paola Bonacina, Christopher A. Lynch and Leonardo de Moura.
On deciding satisfiability by theorem proving with speculative inferences.
- 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.