Theory Multiset_Ordering_in_NP
section ‹Deciding the Generalized Multiset Ordering is in NP›
text ‹We first define a SAT-encoding for the comparison of two multisets w.r.t. two relations S and NS,
then show soundness of the encoding and finally show that the size of the encoding is quadratic in the input.›
theory
Multiset_Ordering_in_NP
imports
Multiset_Ordering_More
Propositional_Formula
begin
subsection ‹Locale for Generic Encoding›
text ‹We first define a generic encoding which may be instantiated for both propositional formulas
and for CNFs. Here, we require some encoding primitives with the semantics specified in the
enc-sound assumptions.›
locale encoder =
fixes eval :: "('a ⇒ bool) ⇒ 'f ⇒ bool"
and enc_False :: "'f"
and enc_True :: 'f
and enc_pos :: "'a ⇒ 'f"
and enc_neg :: "'a ⇒ 'f"
and enc_different :: "'a ⇒ 'a ⇒ 'f"
and enc_equiv_and_not :: "'a ⇒ 'a ⇒ 'a ⇒ 'f"
and enc_equiv_ite :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'f"
and enc_ite :: "'a ⇒ 'a ⇒ 'a ⇒ 'f"
and enc_impl :: "'a ⇒ 'f ⇒ 'f"
and enc_var_impl :: "'a ⇒ 'a ⇒ 'f"
and enc_not_and :: "'a ⇒ 'a ⇒ 'f"
and enc_not_all :: "'a list ⇒ 'f"
and enc_conj :: "'f list ⇒ 'f"
assumes enc_sound[simp]:
"eval α (enc_False) = False"
"eval α (enc_True) = True"
"eval α (enc_pos x) = α x"
"eval α (enc_neg x) = (¬ α x)"
"eval α (enc_different x y) = (α x ≠ α y)"
"eval α (enc_equiv_and_not x y z) = (α x ⟷ α y ∧ ¬ α z)"
"eval α (enc_equiv_ite x y z u) = (α x ⟷ (if α y then α z else α u))"
"eval α (enc_ite x y z) = (if α x then α y else α z)"
"eval α (enc_impl x f) = (α x ⟶ eval α f)"
"eval α (enc_var_impl x y) = (α x ⟶ α y)"
"eval α (enc_not_and x y) = (¬ (α x ∧ α y))"
"eval α (enc_not_all xs) = (¬ (Ball (set xs) α))"
"eval α (enc_conj fs) = (Ball (set fs) (eval α))"
begin
subsection ‹Definition of the Encoding›
text ‹We need to encode formulas of the shape that exactly one variable
is evaluated to true. Here, we use the linear encoding of
\<^cite>‹‹Section~5.3› in "DBLP:journals/jsat/EenS06"›
that requires some auxiliary variables. More precisely, for each
propositional variable that we want to count we require two auxiliary variables.›
fun encode_sum_0_1_main :: "('a × 'a × 'a) list ⇒ 'f list × 'a × 'a" where
"encode_sum_0_1_main [(x, zero, one)] = ([enc_different zero x], zero, x)"
| "encode_sum_0_1_main ((x, zero, one) # rest) = (case encode_sum_0_1_main rest of
(conds, fzero, fone) ⇒ let
czero = enc_equiv_and_not zero fzero x;
cone = enc_equiv_ite one x fzero fone
in (czero # cone # conds, zero, one))"
definition encode_exactly_one :: "('a × 'a × 'a) list ⇒ 'f × 'f list" where
"encode_exactly_one vars = (case vars of [] ⇒ (enc_False, [])
| [(x,_,_)] ⇒ (enc_pos x, [])
| ((x,_,_) # vars) ⇒ (case encode_sum_0_1_main vars of (conds, zero, one)
⇒ (enc_ite x zero one, conds)))"
fun encodeGammaCond :: "'a ⇒ 'a ⇒ bool ⇒ bool ⇒ 'f" where
"encodeGammaCond gam eps True True = enc_True"
| "encodeGammaCond gam eps False False = enc_neg gam"
| "encodeGammaCond gam eps False True = enc_var_impl gam eps"
| "encodeGammaCond gam eps True False = enc_not_and gam eps"
end
text ‹The encoding of the multiset comparisons is based on \<^cite>‹‹Sections~3.6 and 3.7› in "RPO_NP"›.
It uses propositional variables $\gamma_{ij}$ and $\epsilon_i$.
We further add auxiliary variables that are required for the exactly-one-encoding.›