diff options
Diffstat (limited to 'src/Sat.v')
| -rw-r--r-- | src/Sat.v | 580 |
1 files changed, 580 insertions, 0 deletions
diff --git a/src/Sat.v b/src/Sat.v new file mode 100644 index 0000000..1ca3868 --- /dev/null +++ b/src/Sat.v @@ -0,0 +1,580 @@ +(** Homework Assignment 6#<br># +#<a href="http://www.cs.berkeley.edu/~adamc/itp/">#Interactive Computer Theorem +Proving#</a><br># +CS294-9, Fall 2006#<br># +UC Berkeley *) + +(** Submit your solution file for this assignment as an attachment + #<a href="mailto:adamc@cs.berkeley.edu?subject=ICTP HW6">#by e-mail#</a># 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. + + #<a href="HW6.v">#Template source file#</a># + *) + +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 + #<a href="http://en.wikipedia.org/wiki/Boolean_satisfiability_problem">#SAT#</a># + and + #<a href="http://en.wikipedia.org/wiki/DPLL_algorithm">#the DPLL + algorithm#</a>#. 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 #<a href="http://coq.inria.fr/library/Coq.Init.Specif.html">#the + Specif module#</a># 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. + +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). + unfold satLit, upd; simpl; intros. + destruct (eq_nat_dec (snd l) (snd l)); tauto. +Qed. + +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. + unfold satLit, upd; simpl; intros. + destruct (eq_nat_dec v (snd l)); tauto. +Qed. + +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). + unfold satLit, upd; simpl; intros. + destruct (eq_nat_dec v (snd l)); tauto. +Qed. + +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. + unfold satLit, upd; simpl; intros. + destruct (eq_nat_dec (snd l) (snd l)); intuition. + assert False; intuition. +Qed. + +Local Hint Resolve satLit_contra : core. + +(** Here's the tactic that I used to discharge #<i>#all#</i># 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}. + refine (fix setClause (cl: clause) (l: lit) {struct cl} := + match cl with + | nil => inleft (exist _ nil _) + | x :: xs => + match setClause xs l with + | inright p => inright _ + | inleft (exist _ cl' H) => + match eq_nat_dec (snd x) (snd l), bool_eq_dec (fst x) (fst l) with + | left nat_eq, left bool_eq => inright _ + | left eq, right ne => inleft (exist _ cl' _) + | right neq, _ => inleft (exist _ (x :: cl') _) + end + end + end); clear setClause; try magic_solver. + - intros; simpl; left; apply injective_projections in bool_eq; subst; auto. + - split; intros. simpl in H0. inversion H0. eapply satLit_contra; eauto. + destruct x; simpl in *; subst. auto. + apply H. eauto. + simpl. right. apply H; eauto. + - split; intros; simpl in *. inversion H0. destruct x; simpl in *; subst. + left. eauto. + right. apply H. eauto. + inversion H0. left. apply satLit_upd_neq2. auto. auto. + right. apply H. auto. +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. + +(** 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. + *) + +(*Eval compute in setClauseSimple ((false, 1%nat) :: nil) (true, 1%nat).*) +(*Eval compute in setClauseSimple nil (true, 0). +Eval compute in setClauseSimple ((true, 0) :: nil) (true, 0). +Eval compute in setClauseSimple ((true, 0) :: nil) (false, 0). +Eval compute in setClauseSimple ((true, 0) :: nil) (true, 1). +Eval compute in setClauseSimple ((true, 0) :: nil) (false, 1). +Eval compute in setClauseSimple ((true, 0) :: (true, 1) :: nil) (true, 1). +Eval compute in setClauseSimple ((true, 0) :: (true, 1) :: nil) (false, 1). +Eval compute in setClauseSimple ((true, 0) :: (false, 1) :: nil) (true, 1). +Eval compute in setClauseSimple ((true, 0) :: (false, 1) :: nil) (false, 1).*) + +(** It's useful to have this strongly-specified nilness check. *) +Definition isNil : forall (A : Set) (ls : list A), {ls = nil} + {True}. + destruct ls; [left|right]; eauto. +Defined. +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. + +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). + induction cl; simpl; intuition. +Qed. + +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). + induction fm; simpl; intuition. +Qed. + +Local Hint Resolve satLit_idem_formula : core. + +(** 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}. + refine (fix setFormula (fm: formula) (l: lit) {struct fm} := + match fm with + | nil => inleft (exist _ nil _) + | cl' :: fm' => + match setFormula fm' l with + | inright p => inright _ + | inleft (exist _ fm'' H) => + match setClause cl' l with + | inright H' => inleft (exist _ fm'' _) + | inleft (exist _ cl'' _) => + if isNil cl'' + then inright _ + else inleft (exist _ (cl'' :: fm'') _) + end + end + end); clear setFormula; try solve [magic_solver]. +Defined. + +(** 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. + +(*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. + +Local Hint Extern 1 False => + match goal with + | [ H : In _ (_ :: _) |- _ ] => inversion H; clear H; subst + end : core. + +(** 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}. + refine (fix findUnitClause (fm: formula) {struct fm} := + match fm with + | nil => inright _ + | (l :: nil) :: fm' => inleft (exist _ l _) + | cl :: fm' => + match findUnitClause fm' with + | inleft (exist _ l _) => inleft (exist _ l _) + | inright H => inright _ + end + end + ); clear findUnitClause; magic_solver. +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. + induction fm; intuition. + inversion H. + inversion H; subst; simpl in H0; intuition. +Qed. + +Local Hint Resolve unitClauseTrue : core. + +(** 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 (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}). + refine (fix unitPropagate (fm: formula) {struct fm} := + match findUnitClause fm with + | inright H => None + | inleft (exist _ l _) => + match setFormula fm l with + | inright _ => Some (inright _) + | inleft (exist _ fm' _) => + Some (inleft (existT _ fm' (exist _ l _))) + end + end + ); clear unitPropagate; magic_solver. +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. + +(*Eval compute in unitPropagateSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil). +Eval compute in unitPropagateSimple nil. +Eval compute in unitPropagateSimple (((true, 0) :: nil) :: nil). +Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil). +Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 1) :: nil) :: nil). +Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 0) :: (false, 1) :: nil) :: nil). +Eval compute in unitPropagateSimple (((false, 0) :: (false, 1) :: nil) :: ((true, 0) :: nil) :: nil).*) + + +(** * 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). + +Local Hint Unfold satFormula : core. + +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 #<i>#quite#</i># 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}). + 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 (existT _ 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. +Admitted. + +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. + +(*Eval compute in boundedSatSimple 100 nil. +Eval compute in boundedSatSimple 100 (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil). +Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: nil). +Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil). +Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: nil) :: nil). +Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: (false, 0) :: nil) :: nil). +Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((false, 0) :: (false, 0) :: nil) :: ((true, 1) :: nil) :: nil). +Eval compute in boundedSatSimple 100 (((false, 0) :: (true, 1) :: nil) :: ((false, 1) :: (true, 0) :: nil) :: nil).*) |