 SAT solver with a dependent type that guarantees its correctness

Hello,

In chapter Programming with dependent types → Subset types and variations, I faced this exercise:

Implement the DPLL satisfiability decision procedure for boolean formulas in conjunctive normal form, with a dependent type that guarantees its correctness.
An example of a reasonable type for this function would be

∀ f : formula, {truth : tvals | formulaTrue truth f } + {∀ truth, ¬ formulaTrue truth f }.

Implement at least “the basic backtracking algorithm” as defined here:

It might also be instructive to implement the unit propagation and pure literal elimination optimizations described there or some other optimizations that have been used
in modern SAT solvers

Exercise can be found here:

Definition var := nat % type.
Definition partial_map := var -> option bool.
Definition empty : partial_map :=
(fun _ => None).

Definition tvals := partial_map.

Inductive formula : Set :=
| Var : var -> formula
| Not : var -> formula
| Disj : formula -> formula -> formula
| Conj : formula -> formula -> formula.

To keep conjunctive normal form this definition of formula below would be better, I tried both, but in current version I am using first one.

Inductive literal : Set :=
| Var : var -> literal
| Not : var -> literal
| Disj : literal -> literal -> literal.

Inductive formula : Set :=
| Lit : literal -> formula
| Conj : formula -> formula -> formula.

Definition nodup_var := nodup eq_nat_dec.

(* To calculate all vars in formula. *)
Fixpoint vars_in_formula f : list var :=
match f with
| Var v => v :: nil
| Not v => v :: nil
| Disj f1 f2 => nodup_var (vars_in_formula f1 ++ vars_in_formula f2)
| Conj f1 f2 => nodup_var (vars_in_formula f1 ++ vars_in_formula f2)
end.

I can solve task, using maybe type. This is solution:

Inductive maybe (A : Set) (P : A -> Prop) : Set :=
| Unknown : maybe P
| Found : forall x : A, P x -> maybe P.

(* we can define some new notations for convenient usage of type maybe. *)
Notation "{{ x | P }}" := (maybe (fun x => P)).
Notation "??" := (Unknown _ ).
Notation "[| x |]" := (Found _ x _).

Fixpoint evalFormula f (map : tvals) {struct f} : option bool :=
match f with
| Var v => map v
| Not v => match map v with
| Some true => Some false
| Some false => Some true
| None => None (* вовсе не определена функция на мапе? надо бы все None *)
end
| Disj f1 f2 => match (evalFormula f1 map) with
| Some true => match (evalFormula f2 map) with
| Some true => Some true
| Some false => Some true
| None => None
end
| Some false => match (evalFormula f2 map) with
| Some true => Some true
| Some false => Some false
| None => None
end
| None => None (* вовсе не определена функция на мапе? надо бы все None *)
end
| Conj f1 f2 => match (evalFormula f1 map) with
| Some true => match evalFormula f2 map with
| Some true => Some true
| Some false => Some false
| None => None
end
| Some false => match evalFormula f2 map with (* чтоб решить что возвращать, None и *)
| Some true => Some false
| Some false => Some false
| None => None
end
| None => None
end

end.

Definition checkVars : forall (ls : list var) (f : formula) (map : tvals), {{ map' | evalFormula f map' = Some true }}.
refine (fix F (ls : list var) (f : formula) (map : tvals) : {{ map' | evalFormula f map' = Some true }} :=
match ls with
| nil => _
| x :: xs => match F xs f (x !-> Some true; map) with
| ?? => F xs f (x !-> Some false; map)
| res => res
end
end).
destruct (evalFormula f map) eqn:E.
- destruct b.
+ eapply (Found _ map E).
+ apply ??.
- apply ??.
Defined.

Definition f :=  (Disj (Var 1) (Disj (Var 2) (Not 3))).
Eval simpl in checkVars (nodup_var (vars_in_formula f)) f empty.

Definition f1 :=  (Conj (Var 1) (Not 1)).
Eval simpl in checkVars ((vars_in_formula f1)) f1 empty.

See? It works and even works correctly, I can detect if formula is not satisfiable or not, and find tvals (map) which satisfies the formula.

But, Adam Chlipala in his exercise asked to prove a strengthened statement :
∀ f : formula, {truth : tvals | formulaTrue truth f } + {∀ truth, ¬ formulaTrue truth f }.

He asked to prove : ∀ truth, ¬ formulaTrue truth f.

I tried several approaches:
Approach 1

1. create all possible tvals (partial maps), 2. try each one, 3. if no map that satisfies formula found, prove that forall maps formula is unsutisfiable (I failed to do this one),
and this is obviously not a good sulution, cos if we create list of all possible maps, we will not be able to implement optimizations : unit propagation and pure literal elimi-
nation.

Approach 2

• use fuel : create an Axiom that (all possible permutations equals factorial (amount_of_vars_in_formula)), so if all maps checked and we run out of fuel - formula is unsatisfiable forall tvals.
is this a cheating?

Approach 3

• create a lot of dependent types (formula_maps, formula_vars, …). Failed. Couldn’t prove {∀ truth, ¬ formulaTrue truth f }

Below is version with fuel and dependent types (I am working on it now).

Inductive formula_List_Vars : list var -> formula -> Set :=
| FVars_Var : forall v ls, In_var_ls' v ls  = true -> NoDup ls -> formula_List_Vars ls (Var v)
| FVars_Not : forall v ls, In_var_ls' v ls = true -> NoDup ls -> formula_List_Vars ls (Not v)
| FVars_Disj : forall f1 f2 ls1 ls2, NoDup ls1 -> NoDup ls2 ->
formula_List_Vars ls1 f1->
formula_List_Vars ls2 f2 ->
formula_List_Vars (nodup_var (ls1 ++ ls2)) (Disj f1 f2)
| FVars_Conj : forall f1 f2 ls1 ls2, NoDup ls1 -> NoDup ls2 ->
formula_List_Vars ls1 f1 ->
formula_List_Vars ls2 f2 ->
formula_List_Vars (nodup_var (ls1 ++ ls2)) (Conj f1 f2).

Inductive formula_map : tvals -> formula -> Prop :=
| FM_Var : forall map var b, map var = Some b ->
formula_map map (Var var)
| FM_Not : forall map var b, map var = Some b ->
formula_map map (Not var)
| FM_Disj : forall f1 f2 map, formula_map map f1 ->
formula_map map f2 ->
formula_map map (Disj f1 f2)
| FM_Conj : forall f1 f2 map, formula_map map f1 ->
formula_map map f2 ->
formula_map map (Conj f1 f2).

Inductive formulaTrue : tvals -> formula -> Prop :=
| TVar : forall tv var, tv var = Some true -> formula_map tv (Var var) -> formulaTrue tv (Var var)
| TNot : forall tv var, tv var = Some false -> formula_map tv (Not var) -> formulaTrue tv (Not var)
| TDisj : forall f1 f2 tv, formulaTrue tv f1 \/ formulaTrue tv f2 -> formula_map tv f1 -> formula_map tv f2 ->
formulaTrue tv (Disj f1 f2)
| TConj : forall f1 f2 tv, formulaTrue tv f1 -> formulaTrue tv f2 -> formula_map tv f1 -> formula_map tv f2 ->
formulaTrue tv (Conj f1 f2).

Definition checkOneMap (f : formula) (map : tvals) : {formulaTrue map f} + {~formulaTrue map f}. Admitted.

Definition fuel f := fact (length (vars_in_formula f)).
Eval compute in (fuel (Conj (Not 4) (Disj (Var 1) (Not 2)))).

Definition CheckFormulaHelp : forall f (fuel : nat) (ls : list nat) (map : tvals),
{truth : tvals | formulaTrue truth f } + {forall truth, ~formulaTrue truth f }.
refine (fix F f fuel ls map {struct fuel} : {truth : tvals | formulaTrue truth f } + {forall truth, ~formulaTrue truth f } :=
match fuel with
| 0 => _
| S n => match ls return {truth : tvals | formulaTrue truth f } + {forall truth, ~formulaTrue truth f } with
| nil => match (checkOneMap f map) with
| left pf => _
| right pf => _
end
| x :: xs => match F f n xs (x !-> Some true; map) with
| inright _ => F f n xs (x !-> Some false; map)
| res => res
end
end
end).
- right.
- left. exists map. auto.

Definition CheckFormula (f : formula) : {truth : tvals | formulaTrue truth f } + {forall truth, ~ formulaTrue truth f } := @CheckFormulaHelp f (fuel f) (vars_in_formula f) empty.

Also some of my efforts here, all fruitless. sorry for the mess in code.

Thanks,
Natasha

In the type of your fixpoint F within checkVars, I would try to refine the type to tell that the valuation map' returned is an extension of the partial valuation map that you have already chosen, or (in the failure case) that no satisfying valuation extending map exists.

Then in the code of F:

• if the x !-> Some true calls returns with a failure, you know that no extension of map with x = true satisfies the formula
• then you try to call F with x !-> Some false; if this also fails, you know that no extension of map with x = false satisfies the formula
• at this point you know (because x can only be true or false) that no extension of map satisfies the formula

Hello, thank you for the answer.

But what if we have disjunction in the formula,

x \/ y

In this case we don’t care if x is true or false… if y is true, formula is satisfiable.

Thanks.

Also I realized that amount of permutations in this case is not factorial, it should be a power of two.

Your are pointing out that some variables are irrelevant to the satisfiability of the formula. I agree, but I don’t think that it would be an issue. The stronger typing required for this exercise demands that either the solution provides a satisfying valuation/assignment, or that no satisfying valuation exists. If I understand correctly, it does not require the provided valuation to be minimal (to contain only necessary assignment).

With your implementation, if x comes before y in your list of variable, then the algorithm will first try with x !-> Some True, that recursive call will succeed in finding a satisfying valuation, so the returned map will have x !-> Some True, which is not necessary but still correct.