Library HW6

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

Submit your solution file for this assignment as an attachment by e-mail with the subject "ICTP HW6" by the start of class on October 12. You should write your solutions entirely on your own, which includes not consulting any solutions to these problems that may be posted on the web.

Template source file

Require Import Arith Bool List.
This assignment involves building a certified boolean satisfiability solver based on the DPLL algorithm. Your certified procedure will take as input a boolean formula in conjunctive normal form (CNF) and either return a satisfying assignment to the variables or a value signifying that the input formula is unsatisfiable. Moreover, the procedure will be implemented with a rich specification, so you'll know that the answer it gives is correct. By the end of the assignment, you'll have extracted OCaml code that can be used to solve some of the more modest classes of problems in the SATLIB archive.

If you need to page in the relevant background material, try the Wikipedia pages on SAT and the DPLL algorithm. The implementation we'll develop here omits the pure literal heuristic mentioned on the Wikipedia page but is otherwise identical.

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
This is the only section of this assignment where you need to provide your own solutions. You will be implementing four crucial subroutines used by DPLL.

I've provided a number of useful definitions and lemmas which you should feel free to take advantage of in your definitions. A few tips to keep in mind while writing these strongly specified functions:
  • You have a case-by-case choice of a "programming" approach, based around the refine tactic; or a "proving" approach, where the "code" parts of your definitions are constructed step by step with tactics. The former is often harder to get started with, but it tends to be more maintainable.
  • When you use refine with a fix expression, it's usually a good idea to use the clear tactic to remove the recursive function name from the context immediately afterward. This is because Coq won't check that you call this function with strictly smaller arguments until the whole proof is done, and it's a real downer to be told you had an invalid recursion somewhere after you finally "finish" a proof. Instead, make all recursive calls explicit in the refine argument and clear the function name afterward.
  • You'll probably end up with a lot of proof obligations to discharge, and you definitely won't want to prove most of them manually. These tactics will probably be your best friends here: intuition, firstorder, eauto, simpl, subst, .... You will probably want to follow your refine tactics with semicolons and strings of semicolon-separated tactics. These strings should probably start out with basic simplifiers like intros, simpl, and subst.
  • A word of warning about the firstorder tactic: When it works, it works really well! However, this tactic has a way of running forever on complicated enough goals. Be ready to cancel its use (e.g., press the "Stop" button in Proof General) if it takes more than a few seconds. If you do things the way I have, be prepared to mix and match all sorts of different combinations of the automating tactics to get a proof script that solves the problem quickly enough.
  • The dependent type families that we use with rich specifications are all defined in the Specif module of the Coq standard library. One potential gotcha when using them comes from the fact that they are defined inductively with parameters; that is, some arguments to these type families are defined before the colon in the Inductive command. Compared to general arguments stemming from function types after that colon, usage of parameters is restricted; they aren't allowed to vary in recursive occurrences of the type being defined, for instance. Because of this, parameters are ignored for the purposes of pattern-matching, while they must be passed when actually constructing new values. For instance, one would pattern-match a value of a sig type with a pattern like exist x pf, while one would construct a new value of the same type like exist _ x pf. The parameter P is passed in the second case, and we use an underscore when the Coq type-checker ought to be able to infer its value. When this inference isn't possible, you may need to specify manually the predicate defining the sig type you want.


You can also consult the sizeable example at the end of this file, which ties together the pieces you are supposed to write.

You'll probably want to compare booleans for equality at some point.
Definition bool_eq_dec : forall (x y : bool), {x = y} + {x <> y}.
  decide equality.
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.
  intros.
  red in H0, H1.
  simpl in H1.
  subst.
  tauto.
Qed.

Hint Resolve contradictory_assignment.
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).
  unfold satLit, upd; simpl; intros.
  destruct (eq_nat_dec (snd l) (snd l)); tauto.
Qed.

Hint Resolve satLit_upd_eq.

Lemma satLit_upd_neq : forall v l s a,
  v <> snd l
  -> satLit (s, v) (upd a l)
  -> satLit (s, v) a.
  unfold satLit, upd; simpl; intros.
  destruct (eq_nat_dec v (snd l)); tauto.
Qed.

Hint Resolve satLit_upd_neq.

Lemma satLit_upd_neq2 : forall v l s a,
  v <> snd l
  -> satLit (s, v) a
  -> satLit (s, v) (upd a l).
  unfold satLit, upd; simpl; intros.
  destruct (eq_nat_dec v (snd l)); tauto.
Qed.

Hint Resolve satLit_upd_neq2.

Lemma satLit_contra : forall s l a cl,
  s <> fst l
  -> satLit (s, snd l) (upd a l)
  -> satClause cl a.
  unfold satLit, upd; simpl; intros.
  destruct (eq_nat_dec (snd l) (snd l)); intuition.
  assert False; intuition.
Qed.

Hint Resolve satLit_contra.
Here's the tactic that I used to discharge all proof obligations in my implementations of the four functions you will define. It comes with no warranty, as different implementations may lead to obligations that it can't solve, or obligations that it takes 42 years to solve. However, if you think enough like me, each of the four definitions you fill in should read like:
refine some_expression_with_holes; clear function_name; magic_solver.
leaving out the clear invocation for non-recursive function definitions.
Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder;
  match goal with
    | [ H1 : satLit ?l ?a, H2 : satClause ?cl ?a |- _ ] =>
      assert (satClause cl (upd a l)); firstorder
  end.
OK, here's your first challenge. Write this 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}.
Admitted.
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.
When your setClause implementation is done, you should be able to uncomment these test cases and verify that each one yields the correct answer. Be sure that your setClause definition ends in Defined and not Qed, as the former exposes the definition for use in computational reduction, while the latter doesn't.

It's useful to have this strongly-specified nilness check.
Definition isNil : forall (A : Set) (ls : list A), {ls = nil} + {True}.
  destruct ls; eauto.
Defined.
Implicit Arguments isNil [A].
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).
  unfold satLit, upd; simpl; intros.
  destruct (eq_nat_dec (snd l') (snd l)); congruence.
Qed.

Hint Resolve satLit_idem_lit.

Lemma satLit_idem_clause : forall l a cl,
  satLit l a
  -> satClause cl a
  -> satClause cl (upd a l).
  induction cl; simpl; intuition.
Qed.

Hint Resolve satLit_idem_clause.

Lemma satLit_idem_formula : forall l a fm,
  satLit l a
  -> satFormula fm a
  -> satFormula fm (upd a l).
  induction fm; simpl; intuition.
Qed.

Hint Resolve satLit_idem_formula.
Challenge 2: Write this 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}.
Admitted.
Here's some code for testing your implementation.

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

Hint Extern 1 False => discriminate.

Hint Extern 1 False =>
  match goal with
    | [ H : In _ (_ :: _) |- _ ] => inversion H; clear H; subst
  end.
Challenge 3: Write this 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}.
Admitted.
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.
  induction fm; intuition.
  inversion H.
  inversion H; subst; simpl in H0; intuition.
Qed.

Hint Resolve unitClauseTrue.
Final challenge: Implement 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 (sigS (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}).
Admitted.

Definition unitPropagateSimple (fm : formula) :=
  match unitPropagate fm with
    | None => None
    | Some (inleft (existS 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 you've written.

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).

Hint Unfold satFormula.

Lemma satLit_dec : forall l a,
  {satLit l a} + {satLit (negate l) a}.
  destruct l.
  unfold satLit; simpl; intro.
  destruct b; destruct (a v); simpl; auto.
Qed.
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 is not the way you should write proof scripts. ;-)

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 (bound : nat) (fm : formula)
  : option ({al : alist | satFormula fm (interp_alist al)}
    + {forall a, ~satFormula fm a}).
  refine (fix boundedSat (bound : nat) (fm : formula) {struct bound}
    : option ({al : alist | satFormula fm (interp_alist al)}
      + {forall a, ~satFormula fm a}) :=
    match bound with
      | O => None
      | S bound' =>
        if isNil fm
          then Some (inleft _ (exist _ nil _))
          else match unitPropagate fm with
                 | Some (inleft (existS fm' (exist l _))) =>
                   match boundedSat bound' fm' with
                     | None => None
                     | Some (inleft (exist al _)) => Some (inleft _ (exist _ (l :: al) _))
                     | Some (inright _) => Some (inright _ _)
                   end
                 | Some (inright _) => Some (inright _ _)
                 | None =>
                   let l := chooseSplit fm in
                     match setFormula fm l with
                       | inleft (exist fm' _) =>
                         match boundedSat bound' fm' with
                           | None => None
                           | Some (inleft (exist al _)) => Some (inleft _ (exist _ (l :: al) _))
                           | Some (inright _) =>
                             match setFormula fm (negate l) with
                               | inleft (exist fm' _) =>
                                 match boundedSat bound' fm' with
                                   | None => None
                                   | Some (inleft (exist al _)) => Some (inleft _ (exist _ (negate l :: al) _))
                                   | Some (inright _) => Some (inright _ _)
                                 end
                               | inright _ => Some (inright _ _)
                             end
                         end
                       | inright _ =>
                         match setFormula fm (negate l) with
                           | inleft (exist fm' _) =>
                             match boundedSat bound' fm' with
                               | None => None
                               | Some (inleft (exist al _)) => Some (inleft _ (exist _ (negate l :: al) _))
                               | Some (inright _) => Some (inright _ _)
                             end
                           | inright _ => Some (inright _ _)
                         end
                     end
               end
    end); simpl; intros; subst; intuition; try generalize dependent (interp_alist al).
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  assert (satFormula fm (upd a0 l)); firstorder.
  assert (satFormula fm (upd a0 l)); firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
  destruct (satLit_dec l a); intuition eauto;
    assert (satFormula fm (upd a l)); firstorder.
  destruct (satLit_dec l a); intuition eauto;
    assert (satFormula fm (upd a l)); firstorder.
  firstorder.
  firstorder.
  destruct (satLit_dec l a); intuition eauto;
    assert (satFormula fm (upd a (negate l))); firstorder.
  destruct (satLit_dec l a); intuition eauto;
    assert (satFormula fm (upd a (negate l))); firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
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.
We can extract an OCaml version of boundedSat:
Recursive Extraction boundedSat.
You can test the OCaml version by saving the output of the Recursive Extraction to a file Sol6.ml and grabbing the support code in Solver6.ml. In the directory where you've put these files, start ocaml and run:
#use "Sol6.ml";;
#use "Solver6.ml";;
After that, you can solve SAT problems in the SATLIB format. You can find lots of examples in the SATLIB benchmark problem archive. My implementation is quite speedy on the first few classes of formulas listed, so you should be able to test yours on these real problems without much hassle. To solve a problem in file testXX.cnf, run:
solve "testXX.cnf";;
Index
This page has been generated by coqdoc