README.md

itauto: an extensible intuitionistic SAT solver

Context and motivation

The Coq proof assistant features several decision procedures for various logic fragments. For instance, we have:

• tauto for propositional logic
• btauto for boolean logic
• congruence for uninterpreted function symbols (and constructors)
• lia for linear integer arithmetic

However, there is currently no satisfactory scheme for combining the above. The traditional way to combine tauto with congruence is to invoke intuition congruence. This approach is not satistactory because it is neither complete nor efficient.

Example of incompleteness

Consider the following goal:

Goal forall {A: Type} (x y z: A) (p: Prop), x = y -> y = z -> (x = z -> p) -> p.
Proof.
intros.
Fail intuition congruence.
Abort.

intuition is unable to make any propositional progress and therefore calls congruence which is unable to solve the goal. A successful strategy would be to ask congruence to prove x = z; perform modus ponens and conclude.

Example of (non-)efficiency

Consider a smiliar goal where the conclusion is of the form A /\ A.

Goal forall {A: Type} (x y z: A), x = y -> y = z -> x = z /\ x = z.
Proof.
intros.
intuition congruence.
Qed.

In this case, congruence is called twice. A better strategy would be to reuse the proof of x=z. In other words, reuse learned theory clauses along the propositional proof search.

Installation

Installing releases

The recommended way to install the latest released version of itauto is via opam, which will also install all dependencies:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-itauto

Repository installation using opam

The development version of itauto and its dependencies can be installed via opam using the repository:

git clone https://gitlab.inria.fr/fbesson/itauto.git
cd itauto
opam install .

Manual repository installation

To manually build and install the development version of itauto, first install all dependencies:

• Coq
• dune

Then do:

git clone https://gitlab.inria.fr/fbesson/itauto.git
cd itauto
make
make install

Usage

A few relevant tests are found in the test-suite directory.

Require Import Cdcl.Itauto loads the itauto tactic.
Require Import Cdcl.Ctauto loads the itauto tactic and sets the flag Itauto Classic.

itauto tac calls tac when no propositional progress is possible.

Require Import Cdcl.NOlia defines the smt tactic. The smt tactic is itauto using as theory solver a combination à la Nelson-Oppen of congruence and lia (see test-suite/no_test_lia.v).

Require Import Cdcl.NOlra also defines the smt tactic but combine congruence and lra (see test-suite/no_test_lra.v).

When set, the flag Itauto Classic instructs itauto to use the classical axiom Classical.nnpp (only if it present in the environment). This has a positive impact on performance.

Bug report

Do not hesitate to report bugs by email or fill an issue https://gitlab.inria.fr/fbesson/itauto/-/issues .

Internals

A hybrid reflective intuitionitic SMT core

In Coq, we have a reflexive intuitionistic SAT solver parametrised by a theory module. The theory module takes an input a clause of the form

$p_1 \to \dots \to p_n \to q_1 \lor \dots \lor q_n$

and returns and unsat core that is used by the SAT solver for the rest of the proof.

In Ocaml, the SAT solver is run and the theory module wraps an arbitrary Coq tactic. The unsat core being obtained by analysing the proof-term.

Once the SAT solver has succeeded. All the unsat cores are asserted in the original goal. Eventually, the reflexive SAT solver is rerun in Coq using an empty theory.

Design of the sat solver

The SAT solver is intuitionistic but follows the structure of a classic DPLL SAT solver with a few modifications to account for the specificities of intuitionistic logic.

• The input formula is first hash-consed and thus each sub-formula is identified by a unique primitive integer.

• The input formula is transformed using a definitional cnf and we obtain a set of clauses of the following form

  $p_1 \to \dots \to p_n \to q_1 \lor \dots \lor q_n$

After this pre-processing, the SAT solver iterates unit-propgation and case-splits.

• unit propagation is implemented using a variation of head tail pointers.

• When unit propatation is done, the solver branches over a clause of the form

  $q_1 \lor \dots q_n$
  .

• When there is no disjunction to branch over, the solver searches for a literal bound to a formula of the form

  $f \to g$
  and tried to prove
  $g$
  assuming
  $f$
  .

• When no propositional progress is possible, a clause is built and sent to the theory prover. If a conflict clause is generated, the SAT solver continues.

congruence + lia

The combination of congruence and lia is using a black-box Nelson-Oppen scheme. This can be very costly as each tactic is asked to prove a quadratic number of equations.

Future work

• Conflict Driven Clause Learning, beyond backjumping, requires a finer tracking of dependencies to detect the set of input clauses responsible for a conflict.