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"

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 {} = {}"

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]

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"

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
```