Theory TwoSat_Ex

(* Title:      Containers/Examples/TwoSat_Ex.thy
   Author:     Andreas Lochbihler, ETH Zurich
   Author:     Peter Lammich, TU Munich *)

section ‹Formalisation of 2SAT independent of an implementation›

theory TwoSat_Ex imports
  Main
  "HOL-Library.Uprod"
  "Deriving.Compare_Instances" 
begin

type_synonym var = nat
datatype lit = Lit (pos: bool) (var: var)
abbreviation Pos :: "var ⇒ lit" where "Pos ≡ Lit True"
abbreviation Neg :: "var ⇒ lit" where "Neg ≡ Lit False"
type_synonym clause = "lit uprod"
type_synonym cnf = "clause set"

primrec negate :: "lit ⇒ lit"
where "negate (Lit b v) = Lit (¬ b) v"

lemma negate_inject [simp]: "negate x = negate y ⟷ x = y"
by(cases x; cases y) simp

lemma double_negate[simp]: "negate (negate l) = l"
  by (cases l) auto

lemma var_negate[simp]: "var (negate l) = var l"  
  by (cases l) auto


type_synonym valuation = "var ⇒ bool"

definition sat_lit :: "valuation ⇒ lit ⇒ bool"
  where "sat_lit σ l ⟷ (σ (var l) ⟷ pos l)"

lemma sat_lit_alt: "sat_lit σ (Lit p v) ⟷ σ v = p" 
  by (auto simp: sat_lit_def)
  
function sat_clause where
  "sat_clause σ (Upair l1 l2) ⟷ sat_lit σ l1 ∨ sat_lit σ l2"  
  apply (metis surj_pair uprod_exhaust)
  by auto
termination by lexicographic_order
      
definition sat_cnf :: "valuation ⇒ cnf ⇒ bool"  
  where "sat_cnf σ cnf ⟷ (∀cl∈cnf. sat_clause σ cl)"

definition satisfiable :: "cnf ⇒ bool"
where "satisfiable cnf ⟷ (∃σ. sat_cnf σ cnf)"

definition is_2sat :: "cnf ⇒ bool"
where "is_2sat cnf ⟷ (∀cl∈cnf. proper_uprod cl)"

lemma is_2sat_simps [simp]: "is_2sat {}" "is_2sat (insert cl cnf) ⟷ proper_uprod cl ∧ is_2sat cnf"
by(simp_all add: is_2sat_def)
  
lemma negate_sat[simp]: "sat_lit σ (negate l) ⟷ ¬ sat_lit σ l"
  by (cases l) (auto simp: sat_lit_def)
    
function edges_of_clause where 
  "edges_of_clause (Upair l1 l2) = {(negate l1, l2), (negate l2, l1)}"
  by (rule uprod_exhaust) auto
termination by lexicographic_order

definition imp_graph :: "cnf ⇒ (lit × lit) set" where
  "imp_graph cnf = ⋃(edges_of_clause ` cnf)"
  
lemma imp_graph_alt: "imp_graph cnf = {(negate l1,l2) | l1 l2. Upair l1 l2 ∈ cnf}"  
  unfolding imp_graph_def apply safe
  subgoal for l1 l2 cl by (cases cl; clarsimp; metis Upair_inject)
  using edges_of_clause.simps by blast
  
lemma imp_graph_empty [simp]: "imp_graph {} = {}"
  by (simp add: imp_graph_def)

lemma imp_graph_insert [simp]:
  "imp_graph (insert cl cls) = edges_of_clause cl ∪ imp_graph cls"
  by (auto simp: imp_graph_def)
    
lemma imp_graph_skew_sym: 
  "(l⇩1,l⇩2) ∈ imp_graph cnf ⟹ (negate l⇩2, negate l⇩1) ∈ imp_graph cnf"
  unfolding imp_graph_def apply clarsimp 
  subgoal for cl by (cases cl) (auto 4 3 intro: rev_bexI)
  done

lemma imp_graph_rtrancl_skew_sym:    
  "(l⇩1, l⇩2) ∈ (imp_graph cnf)⇧* ⟹ (negate l⇩2, negate l⇩1) ∈ (imp_graph cnf)⇧*"
  by (induction rule: rtrancl.induct)(auto dest: imp_graph_skew_sym)  
      
context
  fixes σ cnf
  assumes sat: "sat_cnf σ cnf"  
begin  
  lemma imp_step:
    assumes S: "sat_lit σ l⇩1"  
    assumes I: "(l⇩1, l⇩2) ∈ imp_graph cnf" 
    shows "sat_lit σ l⇩2"
  proof -
    from I sat have "¬ sat_lit σ l⇩1 ∨ sat_lit σ l⇩2"
      unfolding sat_cnf_def imp_graph_def
      apply clarsimp
      subgoal for x by(cases x)(auto split: if_split_asm)
      done
    with S show ?thesis by simp
  qed 
  
  lemma imp_steps:
    assumes S: "sat_lit σ l⇩1"  
    assumes I: "(l⇩1, l⇩2) ∈ (imp_graph cnf)⇧*" 
    shows "sat_lit σ l⇩2"
    using assms(2,1)
    by (induction) (auto intro: imp_step)  

  lemma ln_loop:
    assumes "(l, negate l) ∈ (imp_graph cnf)⇧*"
    shows "¬ sat_lit σ l"  
    using imp_steps[OF _ assms] 
    by (cases "sat_lit σ l") auto  
  
end

lemma loop_imp_unsat:
  assumes "(Pos x, Neg x) ∈ (imp_graph cnf)⇧*"
  assumes "(Neg x, Pos x) ∈ (imp_graph cnf)⇧*"
  shows "¬ satisfiable cnf"
  using assms ln_loop[of _ cnf "Pos x"] ln_loop[of _ cnf "Neg x"]
  unfolding satisfiable_def by(auto simp add: sat_lit_def)
    
    
(*
  Informal argument why we can find satisfying valuation if
  there are no cycles Pos x →⇧* Neg x →⇧* Pos x.

  Assign all variables as follows:
    Let current assignment be A. By assumption, closed and consistent.
    Choose unassigned variable x
    Try to assign Pos x, form transitive closure.
    If this yields a conflict, assign Neg x

    Assume both Pos x and Neg x would yield conflict:
      As current assignment is always closed, we have 
        G⇧*``Pos x ∩ negate``A = {} and G⇧*``Neg x ∩ negate``A = {}
        (Otherwise:
          Pos x →⇧* negate l, l∈A
          ⟹ l →⇧* Neg x (skew sym)
          ⟹ Neg x ∈ A (A closed, l∈A)
          ⟹ x not unassigned, contr!
        )
      Thus, conflict must be of form:
        Pos x →⇧* Pos y, Pos x →⇧* Neg y
        Neg x →⇧* Pos z, Neg x →⇧* Neg z
        
        ⟹ (skew sym)
          Pos y →⇧* Neg x ⟹ Pos x →⇧* Neg x
          Pos z →⇧* Pos x ⟹ Neg x →⇧* Pos x
          contr to no-cycle assm
*)    
    
definition consistent :: "lit set ⇒ bool" where
  "consistent ls ⟷ (∄x. Pos x ∈ ls ∧ Neg x ∈ ls)"

lemma [simp]: "consistent {}" by (auto simp: consistent_def)  
  
definition vars_of_cnf :: "cnf ⇒ var set" 
where "vars_of_cnf cnf ≡ ⋃cl∈cnf. var ` set_uprod cl"
  
lemma eq_SomeD:
  assumes "x = Eps P"
  assumes "∃x. P x"
  shows "P x"
  using assms by (auto simp: someI)  
  
locale construct_sa =
  fixes cnf :: cnf
  assumes FIN: "finite (vars_of_cnf cnf)"  
  assumes NO_CYC: 
    "∄x. (Pos x, Neg x) ∈ (imp_graph cnf)⇧* ∧ (Neg x, Pos x) ∈ (imp_graph cnf)⇧*"
  assumes TSAT: "is_2sat cnf"
begin  
  abbreviation "G ≡ imp_graph cnf"

  function extend :: "lit set ⇒ lit set" where
    "extend ls = (
      if vars_of_cnf cnf ⊆ var ` ls then ls 
      else let
        x = SOME x. x ∈ vars_of_cnf cnf - var ` ls
      in
        if consistent (ls ∪ G⇧* `` {Pos x}) then
          extend (ls ∪ G⇧* `` {Pos x})
        else
          extend (ls ∪ G⇧* `` {Neg x})
    )"
    by pat_completeness auto
  termination 
    apply (relation "inv_image finite_psubset (λls. vars_of_cnf cnf - var`ls)")
    apply simp
    apply (drule eq_SomeD; auto simp: FIN)  
    apply (drule eq_SomeD; auto simp: FIN)  
    done

  declare extend.simps[simp del]    
      
  lemma extend_vars: "vars_of_cnf cnf ⊆ var ` extend ls" 
    apply (induction ls rule: extend.induct) 
    apply (subst extend.simps)  
    apply (auto split: if_splits simp: Let_def)
    done
      
  lemma extend_cons_closed_aux:
    assumes "consistent ls"
    assumes "G `` ls ⊆ ls"
    shows "consistent (extend ls) ∧ G `` extend ls ⊆ extend ls"  
    using assms(1,2)
  proof (induction ls rule: extend.induct)
    case (1 ls)
      
    show ?case 
    proof (cases "vars_of_cnf cnf ⊆ var`ls")
      case True thus ?thesis using "1.prems"
        by(subst (1 2 3) extend.simps) auto
    next
      case [simp]: False
      define x where "x = (SOME x. x ∈ vars_of_cnf cnf - var ` ls)"  
      with False have XI: "x ∈ vars_of_cnf cnf - var ` ls" 
        by (metis (full_types) DiffI someI_ex subsetI)

      show ?thesis proof (cases "consistent (ls ∪ G⇧*``{Pos x})")
        case CPOS [simp]: True
        from "1.prems" have CL: "G `` (ls ∪ G⇧* `` {Pos x}) ⊆ ls ∪ G⇧* `` {Pos x}"
          by auto
            
        show ?thesis 
          using "1.IH"(1)[OF False x_def CPOS CPOS CL]
          unfolding extend.simps[of ls]
          unfolding x_def[symmetric]
          by auto
      next
        case NCPOS: False
          
        from "1.prems" have CL: "G `` (ls ∪ G⇧* `` {Neg x}) ⊆ ls ∪ G⇧* `` {Neg x}"
          by auto
          
        show ?thesis
        proof (cases "consistent (ls ∪ G⇧* `` {Neg x})")  
          case CNEG[simp]: True
          show ?thesis 
            using "1.IH"(2)[OF False x_def NCPOS CNEG CL] NCPOS
            unfolding extend.simps[of ls] x_def[symmetric]
            by auto
        next
          case NCNEG: False
            
          have X1: "(l, negate l)∈ G⇧*"
            if UNASS: "var l ∉ var ` ls" and "¬ consistent (ls ∪ G⇧* `` {l})" for l
          proof -
            from that(2) obtain y where X1: "Pos y ∈ ls ∪ G⇧*``{l}" "Neg y ∈ ls ∪ G⇧*``{l}"
              unfolding consistent_def by auto
            with "1.prems" have "(l, Pos y) ∈ G⇧* ∨ (l, Neg y) ∈ G⇧*"   
              unfolding consistent_def by auto
            hence X2: "(l, Pos y) ∈ G⇧* ∧ (l, Neg y) ∈ G⇧*"
            proof (safe; rule_tac ccontr)
              assume "(l, Pos y) ∈ G⇧*" "(l, Neg y)∉G⇧*"
              hence "(Neg y,negate l)∈G⇧*" "Neg y ∈ ls" 
                using X1 by (auto dest: imp_graph_rtrancl_skew_sym)
              with CL have "negate l ∈ ls"
                by (metis "1.prems"(2) ImageI Image_closed_trancl)    
              with UNASS show False by (cases l) force+  
            next
              assume "(l, Neg y) ∈ G⇧*" "(l, Pos y) ∉ G⇧*"
              hence "(Pos y, negate l) ∈ G⇧*" "Pos y ∈ ls" 
                using X1 by (auto dest: imp_graph_rtrancl_skew_sym)
              with CL have "negate l ∈ ls"
                by (metis "1.prems"(2) ImageI Image_closed_trancl)    
              with UNASS show False by (cases l) force+  
            qed
            from X2 imp_graph_rtrancl_skew_sym[of _ _ cnf] have "(Neg y, negate l) ∈ G⇧*"
              by force
            with X2 show ?thesis by auto    
          qed
            
          from X1[of "Pos x", OF _ NCPOS] XI have "(Pos x, Neg x)∈G⇧*" by auto  
          moreover from X1[of "Neg x", OF _ NCNEG] XI have "(Neg x, Pos x)∈G⇧*" by auto
          ultimately have False using NO_CYC by blast   
          thus ?thesis by blast
        qed
      qed
    qed
  qed 
    
  lemma extend_cons_closed:
    "consistent (extend {})" 
    "G `` extend {} ⊆ extend {}"  
    using extend_cons_closed_aux[of "{}"] 
    by auto

      
  lemma CCV_sat:
    assumes CONS: "consistent ls"
    assumes CLOSED: "G``ls ⊆ ls"
    assumes VARS: "vars_of_cnf cnf ⊆ var`ls"  
    shows "sat_cnf (λx. Pos x ∈ ls) cnf"  
    unfolding sat_cnf_def
  proof (rule, rule ccontr)
    fix cl
    assume "cl∈cnf"
    with TSAT obtain l1 l2 where [simp]: "cl = Upair l1 l2" "l1 ≠ l2"
      unfolding is_2sat_def
      by(fastforce simp add: proper_uprod_def dest!: bspec split: uprod_split_asm)
      
    assume "¬ sat_clause (λx. Pos x ∈ ls) cl"
    hence "l1 ∉ ls" "l2 ∉ ls" using ‹consistent ls› 
      apply (auto simp: sat_lit_def consistent_def)
      apply (cases l1; cases l2; auto)+
      done  
    
    from VARS ‹cl ∈ cnf› have "var l1 ∈ var ` ls" 
      by (auto 4 3 simp: vars_of_cnf_def)
    with ‹l1 ∉ ls› have "negate l1 ∈ ls"
    proof -
      have "∀L n f. ∃l. ((n::nat) ∉ f ` L ∨ (l::lit) ∈ L) ∧ (n ∉ f ` L ∨ f l = n)"
        by blast
      then show ?thesis
        by (metis (no_types) ‹l1 ∉ ls› ‹var l1 ∈ var ` ls› lit.expand negate_sat var_negate)
    qed

    moreover from ‹cl ∈ cnf› have "(negate l1, l2) ∈ G" 
      unfolding imp_graph_def by(auto intro: rev_bexI)
    ultimately have "l2 ∈ ls" using CLOSED by auto
    thus False using ‹l2 ∉ ls› by auto
  qed

  lemma sat: "satisfiable cnf"
    using CCV_sat[OF extend_cons_closed extend_vars]
    by(auto   simp add: satisfiable_def)
      
end

  
lemma imp_graph_vars:
  assumes "(l, l') ∈ imp_graph cnf"  
  shows "var l ∈ vars_of_cnf cnf" 
  using assms unfolding imp_graph_def vars_of_cnf_def
  apply (clarsimp elim!: rev_bexI)
  subgoal for x by(cases x)(auto split: uprod_split_asm if_split_asm)
  done

theorem finite_2sat_iff:
  assumes FIN: "finite (vars_of_cnf cnf)"
  assumes TSAT: "is_2sat cnf"  
  shows "satisfiable cnf 
    ⟷ (∀x∈vars_of_cnf cnf. 
          ¬ ((Pos x, Neg x) ∈ (imp_graph cnf)⇧* ∧ (Neg x, Pos x) ∈ (imp_graph cnf)⇧* ))"
  apply (safe;clarsimp?; (auto dest: loop_imp_unsat;fail)?)
proof -
  assume " ∀x∈vars_of_cnf cnf.
     (Pos x, Neg x) ∈ (imp_graph cnf)⇧* ⟶ (Neg x, Pos x) ∉ (imp_graph cnf)⇧*"
  then interpret construct_sa cnf
    apply (unfold_locales)
    using FIN TSAT apply auto
    by (metis converse_rtranclE imp_graph_vars lit.inject lit.sel(2))
  
  from sat show "satisfiable cnf" .
qed

derive linorder lit


subsection ‹Finiteness›
definition "lits_of_cnf cnf = Pos`vars_of_cnf cnf ∪ Neg`vars_of_cnf cnf"

lemma inj_on_Pos [simp]: "inj_on Pos A" 
  and inj_on_Neg [simp]: "inj_on Neg A"
by(auto simp add: inj_on_def)

lemma lits_of_cnf_finite[iff]:
  "finite (lits_of_cnf cnf) ⟷ finite (vars_of_cnf cnf)"
proof -
  show ?thesis
    unfolding lits_of_cnf_def 
    by (auto simp: finite_image_iff)
qed  
  
lemma vars_of_cnf_finite[simp, intro]:
  "finite cnf ⟹ finite (vars_of_cnf cnf)"
  unfolding vars_of_cnf_def by auto

lemma lit_eq_negate_conv[simp]:
  "Lit p v = negate l ⟷ l = Lit (¬p) v"
  "negate l = Lit p v ⟷ l = Lit (¬p) v"
  by (cases l; auto)+
  
lemma imp_graph_nodes: "imp_graph cnf ⊆ lits_of_cnf cnf × lits_of_cnf cnf"
  unfolding imp_graph_def
  apply clarsimp
  subgoal for l1 l2 cl 
    by (cases cl; cases l1; cases l2)(fastforce simp: lits_of_cnf_def vars_of_cnf_def)
  done
    
lemma imp_graph_finite[simp, intro]: "finite (vars_of_cnf cnf) ⟹ finite (imp_graph cnf)"
  using finite_subset[OF imp_graph_nodes] by blast

end