Homework Assignment 6 Interactive Computer Theorem Proving CS2949, Fall 2006 UC Berkeley 
Submit your solution file for this assignment as an attachment
by email 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 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 nonrecursive 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 stronglyspecified 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 weaklyspecified 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 and not , as
the former exposes the definition for use in computational reduction, while
the latter doesn't.

It's useful to have this stronglyspecified 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:

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 "timeout" 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
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";;