vericert.hls.Sat

Interactive Computer Theorem Proving
CS294-9, Fall 2006
UC Berkeley

Module Nat_OT := Update_OT Nat_as_OT.
Module NSet := MSetList.Make Nat_OT.

#[local] Open Scope nat.

Problem Definition

Definition var := nat.

We identify propositional variables with natural numbers.

Definition lit := (bool * var)%type.

A literal is a combination of a truth value and a variable.

Definition clause := list lit.

A clause is a list (disjunction) of literals.

Definition formula := list clause.

A formula is a list (conjunction) of clauses.

Definition asgn := var -> bool.

An assignment is a function from variables to their truth values.

Definition satLit (l : lit) (a : asgn) :=
a (snd l) = fst l.

An assignment satisfies a literal if it maps it to true.

Fixpoint satClause (cl : clause) (a : asgn) {struct cl} : Prop :=
  match cl with
  | nil => False
  | l :: cl' => satLit l a \/ satClause cl' a
  end.

An assignment satisfies a clause if it satisfies at least one of its literals.

Fixpoint satFormula (fm: formula) (a: asgn) {struct fm} : Prop :=
  match fm with
  | nil => True
  | cl :: fm' => satClause cl a /\ satFormula fm' a
  end.

An assignment satisfies a formula if it satisfies all of its clauses.

Subroutines

You'll probably want to compare booleans for equality at some point.

Definition bool_eq_dec : forall (x y : bool), {x = y } + {x <> y }.
Defined.

A literal and its negation can't be true simultaneously.

Lemma contradictory_assignment : forall s l cl a,
    s <> fst l
    -> satLit l a
    -> satLit (s , snd l ) a
    -> satClause cl a.

#[local] Hint Resolve contradictory_assignment : core.

Augment an assignment with a new mapping.

Definition upd (a : asgn) (l : lit) : asgn :=
  fun v : var =>
    if eq_nat_dec v (snd l)
    then fst l
    else a v.

Some lemmas about upd

Lemma satLit_upd_eq : forall l a,
    satLit l (upd a l).

#[local] Hint Resolve satLit_upd_eq : core.

Lemma satLit_upd_neq : forall v l s a,
    v <> snd l
    -> satLit (s , v ) (upd a l)
    -> satLit (s , v ) a.

#[local] Hint Resolve satLit_upd_neq : core.

Lemma satLit_upd_neq2 : forall v l s a,
    v <> snd l
    -> satLit (s , v ) a
    -> satLit (s , v ) (upd a l).

#[local] Hint Resolve satLit_upd_neq2 : core.

Lemma satLit_contra : forall s l a cl,
    s <> fst l
    -> satLit (s , snd l ) (upd a l)
    -> satClause cl a.

#[local] Hint Resolve satLit_contra : core.

Strongly-specified function to update a clause to reflect the effect of making a particular literal true.

Definition setClause : forall (cl : clause) (l : lit),
    {cl' : clause |
      forall a, satClause cl (upd a l) <-> satClause cl' a }
    + {forall a, satLit l a -> satClause cl a }.
Defined.

For testing purposes, we define a weakly-specified function as a thin wrapper around setClause.

Definition setClauseSimple (cl : clause) (l : lit) :=
  match setClause cl l with
  | inleft (exist _ cl' _) => Some cl'
  | inright _ => None
  end.

It's useful to have this strongly-specified nilness check.

Definition isNil : forall (A : Set) (ls : list A), {ls = nil } + {True }.
Defined.

Some more lemmas that I found helpful....

Lemma satLit_idem_lit : forall l a l',
    satLit l a
    -> satLit l' a
    -> satLit l' (upd a l).

#[local] Hint Resolve satLit_idem_lit : core.

Lemma satLit_idem_clause : forall l a cl,
    satLit l a
    -> satClause cl a
    -> satClause cl (upd a l).

#[local] Hint Resolve satLit_idem_clause : core.

Lemma satLit_idem_formula : forall l a fm,
    satLit l a
    -> satFormula fm a
    -> satFormula fm (upd a l).

#[local] Hint Resolve satLit_idem_formula : core.

Function that updates an entire formula to reflect setting a literal to true.

Definition setFormula : forall (fm : formula) (l : lit),
    {fm' : formula |
      forall a, satFormula fm (upd a l) <-> satFormula fm' a }
    + {forall a, satLit l a -> ~satFormula fm a }.
Defined.

Definition setFormulaSimple (fm : formula) (l : lit) :=
  match setFormula fm l with
  | inleft (exist _ fm' _) => Some fm'
  | inright _ => None
  end.

Eval compute in setFormulaSimple (((true , 1%nat) :: nil ) :: ((false , 1%nat) :: nil ) :: nil) (true , 1%nat).
Eval compute in setFormulaSimple nil (true , 0).
Eval compute in setFormulaSimple (((true , 0) :: nil ) :: nil) (true , 0).
Eval compute in setFormulaSimple (((false , 0) :: nil ) :: nil) (true , 0).
Eval compute in setFormulaSimple (((false , 1) :: nil ) :: nil) (true , 0).
Eval compute in setFormulaSimple (((false , 1) :: (true , 0) :: nil ) :: nil) (true , 0).
Eval compute in setFormulaSimple (((false , 1) :: (false , 0) :: nil ) :: nil) (true , 0).

#[local] Hint Extern 1 False => discriminate : core.

Code that either finds a unit clause in a formula or declares that there are none.

Definition findUnitClause : forall (fm: formula),
{l : lit | In (l :: nil) fm }
+ {forall l, ~In (l :: nil) fm }.
Defined.

The literal in a unit clause must always be true in a satisfying assignment.

Lemma unitClauseTrue : forall l a fm,
    In (l :: nil) fm
    -> satFormula fm a
    -> satLit l a.

#[local] Hint Resolve unitClauseTrue : core.

Unit propagation. The return type of unitPropagate signifies that three results are possible:

None: There are no unit clauses.
Some (inleft _): There is a unit clause, and here is a formula reflecting setting its literal to true.
Some (inright _): There is a unit clause, and propagating it reveals that the formula is unsatisfiable.

Definition unitPropagate : forall (fm : formula), option (sigT (fun fm' : formula =>
                                                                  {l : lit |
                                                                    (forall a, satFormula fm a -> satLit l a )
                                                                    /\ forall a, satFormula fm (upd a l) <-> satFormula fm' a })
                                                          + {forall a, ~satFormula fm a }).
Defined.

Definition unitPropagateSimple (fm : formula) :=
  match unitPropagate fm with
  | None => None
  | Some (inleft (existT _ fm' (exist _ l _))) => Some (Some (fm', l))
  | Some (inright _) => Some None
  end.

The SAT Solver

This section defines a DPLL SAT solver in terms of the subroutines.

An arbitrary heuristic to choose the next variable to split on

Definition chooseSplit (fm : formula) :=
  match fm with
  | ((l :: _) :: _) => l
  | _ => (true , 0)
  end.

Definition negate (l : lit) := (negb (fst l), snd l ).

#[local] Hint Unfold satFormula : core.

Lemma satLit_dec : forall l a,
    {satLit l a } + {satLit (negate l) a }.

We'll represent assignments as lists of literals instead of functions.

Definition alist := list lit.

Fixpoint interp_alist (al : alist) : asgn :=
  match al with
  | nil => fun _ => true
  | l :: al' => upd (interp_alist al') l
  end.

Here's the final definition!

This implementation isn't quite what you would expect, since it takes an extra parameter expressing a search tree depth. Writing the function without that parameter would be trickier when it came to proving termination. In practice, you can just seed the bound with one plus the number of variables in the input, but the function's return type still indicates a possibility for a "time-out" by returning None.

Definition boundedSat: forall (bound : nat) (fm : formula),
    option ({al : alist | satFormula fm (interp_alist al)}
            + {forall a, ~satFormula fm a }).
Defined.

Definition boundedSatSimple (bound : nat) (fm : formula) :=
  match boundedSat bound fm with
  | None => None
  | Some (inleft (exist _ a _)) => Some (Some a)
  | Some (inright _) => Some None
  end.

Definition lit_set_cl (cl: clause) :=
  fold_right NSet.add NSet.empty (map snd cl).

Definition lit_set (fm: formula) :=
  fold_right NSet.union NSet.empty (map lit_set_cl fm).

Definition sat_measure (fm: formula) := NSet.cardinal (lit_set fm).

Lemma elim_clause :
  forall (cl: clause) l, In l cl -> exists H , setClause cl l = inright H.

Lemma sat_measure_setClause' :
  forall cl cl' l A,
    setClause cl l = inleft (exist _ cl' A) ->
    ~ In (snd l) (map snd cl').

Lemma sat_measure_setClause'' :
  forall cl cl' l A,
    setClause cl l = inleft (exist _ cl' A) ->
    forall l',
      l' <> snd l ->
      In l' (map snd cl) ->
      In l' (map snd cl').

Lemma sat_measure_setClause :
  forall cl cl' l A,
    In (snd l) (map snd cl) ->
    setClause cl l = inleft (exist _ cl' A) ->
    NSet.cardinal (lit_set_cl cl') < NSet.cardinal (lit_set_cl cl).

Definition InFm l (fm: formula) := exists cl , In cl fm /\ In l cl.

Lemma sat_measure_setFormula :
  forall fm fm' l A,
    InFm l fm ->
    setFormula fm l = inleft (exist _ fm' A) ->
    sat_measure fm' < sat_measure fm.

Lemma sat_measure_propagate_unit :
  forall fm' fm H,
    unitPropagate fm = Some (inleft (existT _ fm' H)) ->
    sat_measure fm' < sat_measure fm.

Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }:
  {al : alist | satFormula fm (interp_alist al)} + {forall a, ~satFormula fm a } :=
  if isNil fm
  then inleft _ (exist _ nil _)
  else match unitPropagate fm with
       | Some (inleft (existT _ fm' (exist _ l _))) =>
         match satSolve fm' with
         | inleft (exist _ al _) => inleft _ (exist _ (l :: al) _)
         | inright _ => inright _ _
         end
       | Some (inright _) => inright _ _
       | None =>
         let l := chooseSplit fm in
         match setFormula fm l with
         | inleft (exist _ fm' _) =>
           match satSolve fm' with
           | inleft (exist _ al _) => inleft _ (exist _ (l :: al) _)
           | inright _ =>
             match setFormula fm (negate l) with
             | inleft (exist _ fm' _) =>
               match satSolve fm' with
               | inleft (exist _ al _) => inleft _ (exist _ (negate l :: al) _)
               | inright _ => inright _ _
               end
             | inright _ => inright _ _
             end
           end
         | inright _ =>
           match setFormula fm (negate l) with
           | inleft (exist _ fm' _) =>
             match satSolve fm' with
             | inleft (exist _ al _) => inleft _ (exist _ (negate l :: al) _)
             | inright _ => inright _ _
             end
           | inright _ => inright _ _
           end
         end
       end.
Definition satSolveSimple (fm : formula) :=
  match satSolve fm with
  | inleft (exist _ a _) => Some a
  | inright _ => None
  end.

Eval compute in satSolveSimple nil.