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

 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.

 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.

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

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

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

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

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