SAT solver with a dependent type that guarantees its correctness

Natasha · December 9, 2021, 7:51am

Hello,

I am reading book by Adam Chlipala.
http://adam.chlipala.net/cpdt/cpdt.pdf

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:
http://adam.chlipala.net/cpdt/ex/exercises.pdf

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 am not able to do it, and asking for advice.

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.
  - admit.   
   
Definition CheckFormula (f : formula) : {truth : tvals | formulaTrue truth f } + {forall truth, ~ formulaTrue truth f } := @CheckFormulaHelp f (fuel f) (vars_in_formula f) empty.

I need your advice… hint, direction, ideas…

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

github.com

klausnat/SAT-solver-DPLL-CNF/blob/main/Exercises_04_From_Subset_SAT_Solver.v

Set Implicit Arguments.
Set Asymmetric Patterns.
Require Import Cpdt.CpdtTactics.
Require Import Classical_Prop.
Require Import List.
Require Import Bool.Bool.

Definition var := nat % type. 
Definition total_map := var -> bool.
Definition t_empty : total_map :=
  (fun _ => false).
Definition t_update (m : total_map)
                    (x : var) (v : bool) :=
  fun x' => if PeanoNat.Nat.eqb x x' then v else m x'.
(* to create an empty total map with default value *)
Notation "'_' '!->' v" := t_empty
                            (at level 100, right associativity).
(* extending existing map with some bindings *)
Notation "x '!->' v ';' m" := (t_update m x v)
                              (at level 100, v at next level, right associativity).

This file has been truncated. show original

Thanks,
Natasha

gasche · December 10, 2021, 4:07pm

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

Natasha · December 13, 2021, 5:49am

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.

Natasha · December 13, 2021, 5:52am

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

gasche · December 13, 2021, 9:31am

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.

Natasha · January 5, 2022, 9:07am

Thank you for the answer.
Looks like I am not able to solve this exercise yet.
I could not prove this part of proof.

Topic		Replies	Views
Trouble in implementing dependently typed lookup in Coq using Equations Using Coq coq-equations	2	743	March 7, 2019
Tvals in my code is the total map, why coq insists it is not? Using Coq	3	599	November 2, 2021
How does one access the dependent type unification algorithm from Coq's internals -- especially the one from apply and the substitution solution? Developing plugins	0	447	July 13, 2022
Dependent-typed terms as return values / function parameters Using Coq	3	156	February 2, 2024
Dependent pattern matching with indexed types Using Coq	3	816	January 3, 2020

SAT solver with a dependent type that guarantees its correctness

Related Topics