Start to prove termination of SAT

1 files changed, 266 insertions, 230 deletions

diff --git a/src/hls/Sat.v b/src/hls/Sat.v
index 098eef1..e2bb5dc 100644
--- a/src/hls/Sat.v
+++ b/src/hls/Sat.v
@@ -1,37 +1,18 @@
-(** 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.
+Require Import Coq.funind.Recdef.
+Require Coq.MSets.MSetList.
+Require Import Coq.Structures.OrderedTypeEx.
+Require Import Coq.Structures.OrdersAlt.
+Require Import Coq.Program.Wf.
 
-(** 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.
-  *)
+Module Nat_OT := Update_OT Nat_as_OT.
+Module NSet := MSetList.Make Nat_OT.
 
 
 (** * Problem Definition *)
@@ -57,77 +38,22 @@ Definition satLit (l : lit) (a : asgn) :=
 
 Fixpoint satClause (cl : clause) (a : asgn) {struct cl} : Prop :=
   match cl with
-    | nil => False
-    | l :: cl' => satLit l a \/ satClause cl' a
+  | 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
+  | 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.
@@ -135,10 +61,10 @@ 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.
+    s <> fst l
+    -> satLit l a
+    -> satLit (s, snd l) a
+    -> satClause cl a.
   intros.
   red in H0, H1.
   simpl in H1.
@@ -152,13 +78,13 @@ Qed.
 Definition upd (a : asgn) (l : lit) : asgn :=
   fun v : var =>
     if eq_nat_dec v (snd l)
-      then fst l
-      else a v.
+    then fst l
+    else a v.
 
 (** Some lemmas about [upd] *)
 
 Lemma satLit_upd_eq : forall l a,
-  satLit l (upd a l).
+    satLit l (upd a l).
   unfold satLit, upd; simpl; intros.
   destruct (eq_nat_dec (snd l) (snd l)); tauto.
 Qed.
@@ -166,9 +92,9 @@ 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.
+    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.
@@ -176,9 +102,9 @@ 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).
+    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.
@@ -186,9 +112,9 @@ 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.
+    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.
@@ -196,29 +122,18 @@ 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.
+                     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.
-  *)
+(** 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}.
+    {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 _)
@@ -247,20 +162,13 @@ 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
+  | 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).
@@ -281,9 +189,9 @@ 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).
+    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.
@@ -291,30 +199,28 @@ 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).
+    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).
+    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.
-  *)
+(** 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}.
+    {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 _)
@@ -330,38 +236,34 @@ Definition setFormula : forall (fm : formula) (l : lit),
                   else inleft (exist _ (cl'' :: fm'') _)
                 end
               end
-            end); clear setFormula; try solve [magic_solver].
+            end); clear setFormula; 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
+  | 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 (((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).*)
+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.
+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.
-  *)
+(** 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}.
+    {l : lit | In (l :: nil) fm}
+    + {forall l, ~In (l :: nil) fm}.
   refine (fix findUnitClause (fm: formula) {struct fm} :=
             match fm with
             | nil => inright _
@@ -375,13 +277,11 @@ Definition findUnitClause : forall (fm: formula),
          ); clear findUnitClause; magic_solver.
 Defined.
 
-(** The literal in a unit clause must always be true in a satisfying
-  assignment.
-  *)
+(** 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.
+    In (l :: nil) fm
+    -> satFormula fm a
+    -> satLit l a.
   induction fm; intuition.
   inversion H.
   inversion H; subst; simpl in H0; intuition.
@@ -389,19 +289,18 @@ Qed.
 
 #[local] Hint Resolve unitClauseTrue : core.
 
-(** Final challenge: Implement unit propagation.  The return type of
-  [unitPropagate] signifies that three results are possible:
+(** 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}).
+                                                                  {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
@@ -418,9 +317,9 @@ 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
+  | 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).
@@ -434,15 +333,13 @@ Eval compute in unitPropagateSimple (((false, 0) :: (false, 1) :: nil) :: ((true
 
 (** * The SAT Solver *)
 
-(** This section defines a DPLL SAT solver in terms of the subroutines you've
-  written.
-  *)
+(** 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)
+  | ((l :: _) :: _) => l
+  | _ => (true, 0)
   end.
 
 Definition negate (l : lit) := (negb (fst l), snd l).
@@ -450,7 +347,7 @@ 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}.
+    {satLit l a} + {satLit (negate l) a}.
   destruct l.
   unfold satLit; simpl; intro.
   destruct b; destruct (a v); simpl; auto.
@@ -461,12 +358,11 @@ Definition alist := list lit.
 
 Fixpoint interp_alist (al : alist) : asgn :=
   match al with
-    | nil => fun _ => true
-    | l :: al' => upd (interp_alist al') l
+  | 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. ;-)
+(** Here's the final definition!
 
   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
@@ -474,57 +370,57 @@ Fixpoint interp_alist (al : alist) : asgn :=
   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}).
+    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
+          : 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
+                     end
+                   | Some (inright _) => Some (inright _ _)
+                   | None =>
+                     let l := chooseSplit fm in
                      match setFormula fm l with
-                       | inleft (exist _ fm' _) =>
-                         match boundedSat bound' fm' 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 _ (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
+                           | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
+                           | Some (inright _) => Some (inright _ _)
+                           end
+                         | inright _ => Some (inright _ _)
                          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
+                     | 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).
+                   end
+            end); simpl; intros; subst; intuition; try generalize dependent (interp_alist al).
   firstorder.
   firstorder.
   firstorder.
@@ -578,3 +474,143 @@ Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true
 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).*)
+
+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).
+
+Compute lit_set (((true, 1)::(true, 2)::(true, 1)::nil)::nil).
+
+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.
+Proof.
+  induction cl; intros; simpl in *; try contradiction.
+  destruct (setClause cl l) eqn:?; [|econstructor; eauto].
+  destruct s. inversion H; subst. clear H.
+  destruct (Nat.eq_dec (snd l) (snd l)); [| contradiction].
+  destruct (bool_eq_dec (fst l) (fst l)); [| contradiction].
+  econstructor. eauto. apply IHcl in H0.
+  inversion H0. rewrite H1 in Heqs. discriminate.
+Qed.
+
+Lemma sat_measure_propagate_unit :
+  forall fm' fm l
+         (i: forall a : asgn, satFormula fm (upd a l) <-> satFormula fm' a)
+         (s: forall a : asgn, satFormula fm a -> satLit l a),
+    Some
+      (inleft
+         (existT
+            (fun fm' : formula =>
+               {l : lit
+                 | (forall a : asgn, satFormula fm a -> satLit l a) /\
+                   (forall a : asgn, satFormula fm (upd a l) <-> satFormula fm' a)}) fm'
+            (exist
+               (fun l : lit =>
+                  (forall a : asgn, satFormula fm a -> satLit l a) /\
+                  (forall a : asgn, satFormula fm (upd a l) <-> satFormula fm' a)) l
+               (conj s i)))) = unitPropagate fm ->
+    sat_measure fm' < sat_measure fm.
+Proof.
+  induction fm.
+  - intros. simpl in *. discriminate.
+  - intros.
+    Admitted.
+
+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.
+Next Obligation.
+  eapply sat_measure_propagate_unit; eauto. Defined.
+Next Obligation.
+  apply i; auto. Defined.
+Next Obligation.
+  unfold not; intros; eapply wildcard'; apply i; eauto. Defined.
+Next Obligation.
+  Admitted.
+Next Obligation.
+  apply wildcard'0; auto. Defined.
+Next Obligation.
+  Admitted.
+Next Obligation.
+  apply wildcard'2; auto. Defined.
+Next Obligation.
+  unfold not in *; intros.
+  destruct (satLit_dec (chooseSplit fm) a);
+  [assert (satFormula fm (upd a (chooseSplit fm)))
+  | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; firstorder.
+  { eapply wildcard'1. apply wildcard'0; eauto. }
+  { eapply wildcard'. apply wildcard'2; eauto. }
+Defined.
+Next Obligation.
+  unfold not in *; intros.
+  destruct (satLit_dec (chooseSplit fm) a);
+  [assert (satFormula fm (upd a (chooseSplit fm)))
+  | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; firstorder.
+  { eapply wildcard'1. eapply wildcard'0. eauto. }
+  { eapply wildcard'; eauto. }
+Defined.
+Next Obligation.
+  Admitted.
+Next Obligation.
+  apply wildcard'1; auto. Defined.
+Next Obligation.
+  unfold not in *; intros.
+  destruct (satLit_dec (chooseSplit fm) a);
+  [assert (satFormula fm (upd a (chooseSplit fm)))
+  | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; firstorder.
+  { eapply wildcard'0; eauto. }
+  { eapply wildcard'; apply wildcard'1; eauto. }
+Defined.
+Next Obligation.
+  unfold not in *; intros.
+  destruct (satLit_dec (chooseSplit fm) a).
+  { eapply wildcard'0; eauto. }
+  { eapply wildcard'; eauto. }
+Defined.
+
+Definition satSolveSimple (fm : formula) :=
+  match satSolve fm with
+  | inleft (exist _ a _) => Some a
+  | inright _ => None
+  end.
+
+Eval compute in satSolveSimple nil.