Theory NieuwenhuisOliverasTinelli
section‹Transition system of Nieuwenhuis, Oliveras and Tinelli.›
theory NieuwenhuisOliverasTinelli
imports SatSolverVerification
begin
text‹This theory formalizes the transition rule system given by
Nieuwenhuis et al. in \<^cite>‹"NieuwenhuisOliverasTinelli"››
subsection‹Specification›
record State =
"getF" :: Formula
"getM" :: LiteralTrail
definition
appliedDecide:: "State ⇒ State ⇒ Variable set ⇒ bool"
where
"appliedDecide stateA stateB decisionVars ==
∃ l.
(var l) ∈ decisionVars ∧
¬ l el (elements (getM stateA)) ∧
¬ opposite l el (elements (getM stateA)) ∧
getF stateB = getF stateA ∧
getM stateB = getM stateA @ [(l, True)]
"
definition
applicableDecide :: "State ⇒ Variable set ⇒ bool"
where
"applicableDecide state decisionVars == ∃ state'. appliedDecide state state' decisionVars"
definition
appliedUnitPropagate :: "State ⇒ State ⇒ bool"
where
"appliedUnitPropagate stateA stateB ==
∃ (uc::Clause) (ul::Literal).
uc el (getF stateA) ∧
isUnitClause uc ul (elements (getM stateA)) ∧
getF stateB = getF stateA ∧
getM stateB = getM stateA @ [(ul, False)]
"
definition
applicableUnitPropagate :: "State ⇒ bool"
where
"applicableUnitPropagate state == ∃ state'. appliedUnitPropagate state state'"
definition
appliedBackjump :: "State ⇒ State ⇒ bool"
where
"appliedBackjump stateA stateB ==
∃ bc bl level.
isUnitClause bc bl (elements (prefixToLevel level (getM stateA))) ∧
formulaEntailsClause (getF stateA) bc ∧
var bl ∈ vars (getF stateA) ∪ vars (elements (getM stateA)) ∧
0 ≤ level ∧ level < (currentLevel (getM stateA)) ∧
getF stateB = getF stateA ∧
getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]
"
definition
applicableBackjump :: "State ⇒ bool"
where
"applicableBackjump state == ∃ state'. appliedBackjump state state'"
definition
appliedLearn :: "State ⇒ State ⇒ bool"
where
"appliedLearn stateA stateB ==
∃ c.
(formulaEntailsClause (getF stateA) c) ∧
(vars c) ⊆ vars (getF stateA) ∪ vars (elements (getM stateA)) ∧
getF stateB = getF stateA @ [c] ∧
getM stateB = getM stateA
"
definition
applicableLearn :: "State ⇒ bool"
where
"applicableLearn state == (∃ state'. appliedLearn state state')"
text‹Solving starts with the initial formula and the empty trail.›
definition
isInitialState :: "State ⇒ Formula ⇒ bool"
where
"isInitialState state F0 ==
getF state = F0 ∧
getM state = []
"
text‹Transitions are preformed only by using given rules.›
definition
"transition stateA stateB decisionVars ==
appliedDecide stateA stateB decisionVars ∨
appliedUnitPropagate stateA stateB ∨
appliedLearn stateA stateB ∨
appliedBackjump stateA stateB
"
text‹Transition relation is obtained by applying transition rules
iteratively. It is defined using a reflexive-transitive closure.›
definition
"transitionRelation decisionVars == ({(stateA, stateB). transition stateA stateB decisionVars})^*"
text‹Final state is one in which no rules apply›
definition
isFinalState :: "State ⇒ Variable set ⇒ bool"
where
"isFinalState state decisionVars == ¬ (∃ state'. transition state state' decisionVars)"
text‹The following several lemmas establish conditions for applicability of different rules.›
lemma applicableDecideCharacterization:
fixes stateA::State
shows "applicableDecide stateA decisionVars =
(∃ l.
(var l) ∈ decisionVars ∧
¬ l el (elements (getM stateA)) ∧
¬ opposite l el (elements (getM stateA)))
" (is "?lhs = ?rhs")
proof
assume ?rhs
then obtain l where
*: "(var l) ∈ decisionVars" "¬ l el (elements (getM stateA))" "¬ opposite l el (elements (getM stateA))"
unfolding applicableDecide_def
by auto
let ?stateB = "stateA⦇ getM := (getM stateA) @ [(l, True)] ⦈"
from * have "appliedDecide stateA ?stateB decisionVars"
unfolding appliedDecide_def
by auto
thus ?lhs
unfolding applicableDecide_def
by auto
next
assume ?lhs
then obtain stateB l
where "(var l) ∈ decisionVars" "¬ l el (elements (getM stateA))"
"¬ opposite l el (elements (getM stateA))"
unfolding applicableDecide_def
unfolding appliedDecide_def
by auto
thus ?rhs
by auto
qed
lemma applicableUnitPropagateCharacterization:
fixes stateA::State and F0::Formula
shows "applicableUnitPropagate stateA =
(∃ (uc::Clause) (ul::Literal).
uc el (getF stateA) ∧
isUnitClause uc ul (elements (getM stateA)))
" (is "?lhs = ?rhs")
proof
assume "?rhs"
then obtain ul uc
where *: "uc el (getF stateA)" "isUnitClause uc ul (elements (getM stateA))"
unfolding applicableUnitPropagate_def
by auto
let ?stateB = "stateA⦇ getM := getM stateA @ [(ul, False)] ⦈"
from * have "appliedUnitPropagate stateA ?stateB"
unfolding appliedUnitPropagate_def
by auto
thus ?lhs
unfolding applicableUnitPropagate_def
by auto
next
assume ?lhs
then obtain stateB uc ul
where "uc el (getF stateA)" "isUnitClause uc ul (elements (getM stateA))"
unfolding applicableUnitPropagate_def
unfolding appliedUnitPropagate_def
by auto
thus ?rhs
by auto
qed
lemma applicableBackjumpCharacterization:
fixes stateA::State
shows "applicableBackjump stateA =
(∃ bc bl level.
isUnitClause bc bl (elements (prefixToLevel level (getM stateA))) ∧
formulaEntailsClause (getF stateA) bc ∧
var bl ∈ vars (getF stateA) ∪ vars (elements (getM stateA)) ∧
0 ≤ level ∧ level < (currentLevel (getM stateA)))" (is "?lhs = ?rhs")
proof
assume "?rhs"
then obtain bc bl level
where *: "isUnitClause bc bl (elements (prefixToLevel level (getM stateA)))"
"formulaEntailsClause (getF stateA) bc"
"var bl ∈ vars (getF stateA) ∪ vars (elements (getM stateA))"
"0 ≤ level" "level < (currentLevel (getM stateA))"
unfolding applicableBackjump_def
by auto
let ?stateB = "stateA⦇ getM := prefixToLevel level (getM stateA) @ [(bl, False)]⦈"
from * have "appliedBackjump stateA ?stateB"
unfolding appliedBackjump_def
by auto
thus "?lhs"
unfolding applicableBackjump_def
by auto
next
assume "?lhs"
then obtain stateB
where "appliedBackjump stateA stateB"
unfolding applicableBackjump_def
by auto
then obtain bc bl level
where "isUnitClause bc bl (elements (prefixToLevel level (getM stateA)))"
"formulaEntailsClause (getF stateA) bc"
"var bl ∈ vars (getF stateA) ∪ vars (elements (getM stateA))"
"getF stateB = getF stateA"
"getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]"
"0 ≤ level" "level < (currentLevel (getM stateA))"
unfolding appliedBackjump_def
by auto
thus "?rhs"
by auto
qed
lemma applicableLearnCharacterization:
fixes stateA::State
shows "applicableLearn stateA =
(∃ c. formulaEntailsClause (getF stateA) c ∧
vars c ⊆ vars (getF stateA) ∪ vars (elements (getM stateA)))" (is "?lhs = ?rhs")
proof
assume "?rhs"
then obtain c where
*: "formulaEntailsClause (getF stateA) c"
"vars c ⊆ vars (getF stateA) ∪ vars (elements (getM stateA))"
unfolding applicableLearn_def
by auto
let ?stateB = "stateA⦇ getF := getF stateA @ [c]⦈"
from * have "appliedLearn stateA ?stateB"
unfolding appliedLearn_def
by auto
thus "?lhs"
unfolding applicableLearn_def
by auto
next
assume "?lhs"
then obtain c stateB
where
"formulaEntailsClause (getF stateA) c"
"vars c ⊆ vars (getF stateA) ∪ vars (elements (getM stateA))"
unfolding applicableLearn_def
unfolding appliedLearn_def
by auto
thus "?rhs"
by auto
qed
text‹Final states are the ones where no rule is applicable.›
lemma finalStateNonApplicable:
fixes state::State
shows "isFinalState state decisionVars =
(¬ applicableDecide state decisionVars ∧
¬ applicableUnitPropagate state ∧
¬ applicableBackjump state ∧
¬ applicableLearn state)"
unfolding isFinalState_def
unfolding transition_def
unfolding applicableDecide_def
unfolding applicableUnitPropagate_def
unfolding applicableBackjump_def
unfolding applicableLearn_def
by auto
subsection‹Invariants›
text‹Invariants that are relevant for the rest of correctness proof.›
definition
invariantsHoldInState :: "State ⇒ Formula ⇒ Variable set ⇒ bool"
where
"invariantsHoldInState state F0 decisionVars ==
InvariantImpliedLiterals (getF state) (getM state) ∧
InvariantVarsM (getM state) F0 decisionVars ∧
InvariantVarsF (getF state) F0 decisionVars ∧
InvariantConsistent (getM state) ∧
InvariantUniq (getM state) ∧
InvariantEquivalent F0 (getF state)
"
text‹Invariants hold in initial states.›
lemma invariantsHoldInInitialState:
fixes state :: State and F0 :: Formula
assumes "isInitialState state F0"
shows "invariantsHoldInState state F0 decisionVars"
using assms
by (auto simp add:
isInitialState_def
invariantsHoldInState_def
InvariantImpliedLiterals_def
InvariantVarsM_def
InvariantVarsF_def
InvariantConsistent_def
InvariantUniq_def
InvariantEquivalent_def equivalentFormulae_def
)
text‹Valid transitions preserve invariants.›
lemma transitionsPreserveInvariants:
fixes stateA::State and stateB::State
assumes "transition stateA stateB decisionVars" and
"invariantsHoldInState stateA F0 decisionVars"
shows "invariantsHoldInState stateB F0 decisionVars"
proof-
from ‹invariantsHoldInState stateA F0 decisionVars›
have
"InvariantImpliedLiterals (getF stateA) (getM stateA)" and
"InvariantVarsM (getM stateA) F0 decisionVars" and
"InvariantVarsF (getF stateA) F0 decisionVars" and
"InvariantConsistent (getM stateA)" and
"InvariantUniq (getM stateA)" and
"InvariantEquivalent F0 (getF stateA)"
unfolding invariantsHoldInState_def
by auto
{
assume "appliedDecide stateA stateB decisionVars"
then obtain l::Literal where
"(var l) ∈ decisionVars"
"¬ literalTrue l (elements (getM stateA))"
"¬ literalFalse l (elements (getM stateA))"
"getM stateB = getM stateA @ [(l, True)]"
"getF stateB = getF stateA"
unfolding appliedDecide_def
by auto
from ‹¬ literalTrue l (elements (getM stateA))› ‹¬ literalFalse l (elements (getM stateA))›
have *: "var l ∉ vars (elements (getM stateA))"
using variableDefinedImpliesLiteralDefined[of "l" "elements (getM stateA)"]
by simp
have "InvariantImpliedLiterals (getF stateB) (getM stateB)"
using ‹getF stateB = getF stateA›
‹getM stateB = getM stateA @ [(l, True)]›
‹InvariantImpliedLiterals (getF stateA) (getM stateA)›
‹InvariantUniq (getM stateA)›
‹var l ∉ vars (elements (getM stateA))›
InvariantImpliedLiteralsAfterDecide[of "getF stateA" "getM stateA" "l" "getM stateB"]
by simp
moreover
have "InvariantVarsM (getM stateB) F0 decisionVars"
using ‹getM stateB = getM stateA @ [(l, True)]›
‹InvariantVarsM (getM stateA) F0 decisionVars›
‹var l ∈ decisionVars›
InvariantVarsMAfterDecide[of "getM stateA" "F0" "decisionVars" "l" "getM stateB"]
by simp
moreover
have "InvariantVarsF (getF stateB) F0 decisionVars"
using ‹getF stateB = getF stateA›
‹InvariantVarsF (getF stateA) F0 decisionVars›
by simp
moreover
have "InvariantConsistent (getM stateB)"
using ‹getM stateB = getM stateA @ [(l, True)]›
‹InvariantConsistent (getM stateA)›
‹var l ∉ vars (elements (getM stateA))›
InvariantConsistentAfterDecide[of "getM stateA" "l" "getM stateB"]
by simp
moreover
have "InvariantUniq (getM stateB)"
using ‹getM stateB = getM stateA @ [(l, True)]›
‹InvariantUniq (getM stateA)›
‹var l ∉ vars (elements (getM stateA))›
InvariantUniqAfterDecide[of "getM stateA" "l" "getM stateB"]
by simp
moreover
have "InvariantEquivalent F0 (getF stateB)"
using ‹getF stateB = getF stateA›
‹InvariantEquivalent F0 (getF stateA)›
by simp
ultimately
have ?thesis
unfolding invariantsHoldInState_def
by auto
}
moreover
{
assume "appliedUnitPropagate stateA stateB"
then obtain uc::Clause and ul::Literal where
"uc el (getF stateA)"
"isUnitClause uc ul (elements (getM stateA))"
"getF stateB = getF stateA"
"getM stateB = getM stateA @ [(ul, False)]"
unfolding appliedUnitPropagate_def
by auto
from ‹isUnitClause uc ul (elements (getM stateA))›
have "ul el uc"
unfolding isUnitClause_def
by simp
from ‹uc el (getF stateA)›
have "formulaEntailsClause (getF stateA) uc"
by (simp add: formulaEntailsItsClauses)
have "InvariantImpliedLiterals (getF stateB) (getM stateB)"
using ‹getF stateB = getF stateA›
‹InvariantImpliedLiterals (getF stateA) (getM stateA)›
‹formulaEntailsClause (getF stateA) uc›
‹isUnitClause uc ul (elements (getM stateA))›
‹getM stateB = getM stateA @ [(ul, False)]›
InvariantImpliedLiteralsAfterUnitPropagate[of "getF stateA" "getM stateA" "uc" "ul" "getM stateB"]
by simp
moreover
from ‹ul el uc› ‹uc el (getF stateA)›
have "ul el (getF stateA)"
by (auto simp add: literalElFormulaCharacterization)
with ‹InvariantVarsF (getF stateA) F0 decisionVars›
have "var ul ∈ vars F0 ∪ decisionVars"
using "formulaContainsItsLiteralsVariable" [of "ul" "getF stateA"]
unfolding InvariantVarsF_def
by auto
have "InvariantVarsM (getM stateB) F0 decisionVars"
using ‹InvariantVarsM (getM stateA) F0 decisionVars›
‹var ul ∈ vars F0 ∪ decisionVars›
‹getM stateB = getM stateA @ [(ul, False)]›
InvariantVarsMAfterUnitPropagate[of "getM stateA" "F0" "decisionVars" "ul" "getM stateB"]
by simp
moreover
have "InvariantVarsF (getF stateB) F0 decisionVars"
using ‹getF stateB = getF stateA›
‹InvariantVarsF (getF stateA) F0 decisionVars›
by simp
moreover
have "InvariantConsistent (getM stateB)"
using ‹InvariantConsistent (getM stateA)›
‹isUnitClause uc ul (elements (getM stateA))›
‹getM stateB = getM stateA @ [(ul, False)]›
InvariantConsistentAfterUnitPropagate [of "getM stateA" "uc" "ul" "getM stateB"]
by simp
moreover
have "InvariantUniq (getM stateB)"
using ‹InvariantUniq (getM stateA)›
‹isUnitClause uc ul (elements (getM stateA))›
‹getM stateB = getM stateA @ [(ul, False)]›
InvariantUniqAfterUnitPropagate [of "getM stateA" "uc" "ul" "getM stateB"]
by simp
moreover
have "InvariantEquivalent F0 (getF stateB)"
using ‹getF stateB = getF stateA›
‹InvariantEquivalent F0 (getF stateA)›
by simp
ultimately
have ?thesis
unfolding invariantsHoldInState_def
by auto
}
moreover
{
assume "appliedLearn stateA stateB"
then obtain c::Clause where
"formulaEntailsClause (getF stateA) c"
"vars c ⊆ vars (getF stateA) ∪ vars (elements (getM stateA))"
"getF stateB = getF stateA @ [c]"
"getM stateB = getM stateA"
unfolding appliedLearn_def
by auto
have "InvariantImpliedLiterals (getF stateB) (getM stateB)"
using
‹InvariantImpliedLiterals (getF stateA) (getM stateA)›
‹getF stateB = getF stateA @ [c]›
‹getM stateB = getM stateA›
InvariantImpliedLiteralsAfterLearn[of "getF stateA" "getM stateA" "getF stateB"]
by simp
moreover
have "InvariantVarsM (getM stateB) F0 decisionVars"
using
‹InvariantVarsM (getM stateA) F0 decisionVars›
‹getM stateB = getM stateA›
by simp
moreover
from ‹vars c ⊆ vars (getF stateA) ∪ vars (elements (getM stateA))›
‹InvariantVarsM (getM stateA) F0 decisionVars›
‹InvariantVarsF (getF stateA) F0 decisionVars›
have "vars c ⊆ vars F0 ∪ decisionVars"
unfolding InvariantVarsM_def
unfolding InvariantVarsF_def
by auto
hence "InvariantVarsF (getF stateB) F0 decisionVars"
using ‹InvariantVarsF (getF stateA) F0 decisionVars›
‹getF stateB = getF stateA @ [c]›
using varsAppendFormulae [of "getF stateA" "[c]"]
unfolding InvariantVarsF_def
by simp
moreover
have "InvariantConsistent (getM stateB)"
using ‹InvariantConsistent (getM stateA)›
‹getM stateB = getM stateA›
by simp
moreover
have "InvariantUniq (getM stateB)"
using ‹InvariantUniq (getM stateA)›
‹getM stateB = getM stateA›
by simp
moreover
have "InvariantEquivalent F0 (getF stateB)"
using
‹InvariantEquivalent F0 (getF stateA)›
‹formulaEntailsClause (getF stateA) c›
‹getF stateB = getF stateA @ [c]›
InvariantEquivalentAfterLearn[of "F0" "getF stateA" "c" "getF stateB"]
by simp
ultimately
have ?thesis
unfolding invariantsHoldInState_def
by simp
}
moreover
{
assume "appliedBackjump stateA stateB"
then obtain bc::Clause and bl::Literal and level::nat
where
"isUnitClause bc bl (elements (prefixToLevel level (getM stateA)))"
"formulaEntailsClause (getF stateA) bc"
"var bl ∈ vars (getF stateA) ∪ vars (elements (getM stateA))"
"getF stateB = getF stateA"
"getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]"
unfolding appliedBackjump_def
by auto
have "isPrefix (prefixToLevel level (getM stateA)) (getM stateA)"
by (simp add:isPrefixPrefixToLevel)
have "InvariantImpliedLiterals (getF stateB) (getM stateB)"
using ‹InvariantImpliedLiterals (getF stateA) (getM stateA)›
‹isPrefix (prefixToLevel level (getM stateA)) (getM stateA)›
‹isUnitClause bc bl (elements (prefixToLevel level (getM stateA)))›
‹formulaEntailsClause (getF stateA) bc›
‹getF stateB = getF stateA›
‹getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]›
InvariantImpliedLiteralsAfterBackjump[of "getF stateA" "getM stateA" "prefixToLevel level (getM stateA)" "bc" "bl" "getM stateB"]
by simp
moreover
from ‹InvariantVarsF (getF stateA) F0 decisionVars›
‹InvariantVarsM (getM stateA) F0 decisionVars›
‹var bl ∈ vars (getF stateA) ∪ vars (elements (getM stateA))›
have "var bl ∈ vars F0 ∪ decisionVars"
unfolding InvariantVarsM_def
unfolding InvariantVarsF_def
by auto
have "InvariantVarsM (getM stateB) F0 decisionVars"
using ‹InvariantVarsM (getM stateA) F0 decisionVars›
‹isPrefix (prefixToLevel level (getM stateA)) (getM stateA)›
‹getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]›
‹var bl ∈ vars F0 ∪ decisionVars›
InvariantVarsMAfterBackjump[of "getM stateA" "F0" "decisionVars" "prefixToLevel level (getM stateA)" "bl" "getM stateB"]
by simp
moreover
have "InvariantVarsF (getF stateB) F0 decisionVars"
using ‹getF stateB = getF stateA›
‹InvariantVarsF (getF stateA) F0 decisionVars›
by simp
moreover
have "InvariantConsistent (getM stateB)"
using ‹InvariantConsistent (getM stateA)›
‹isPrefix (prefixToLevel level (getM stateA)) (getM stateA)›
‹isUnitClause bc bl (elements (prefixToLevel level (getM stateA)))›
‹getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]›
InvariantConsistentAfterBackjump[of "getM stateA" "prefixToLevel level (getM stateA)" "bc" "bl" "getM stateB"]
by simp
moreover
have "InvariantUniq (getM stateB)"
using ‹InvariantUniq (getM stateA)›
‹isPrefix (prefixToLevel level (getM stateA)) (getM stateA)›
‹isUnitClause bc bl (elements (prefixToLevel level (getM stateA)))›
‹getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]›
InvariantUniqAfterBackjump[of "getM stateA" "prefixToLevel level (getM stateA)" "bc" "bl" "getM stateB"]
by simp
moreover
have "InvariantEquivalent F0 (getF stateB)"
using
‹InvariantEquivalent F0 (getF stateA)›
‹getF stateB = getF stateA›
by simp
ultimately
have ?thesis
unfolding invariantsHoldInState_def
by auto
}
ultimately
show ?thesis
using ‹transition stateA stateB decisionVars›
unfolding transition_def
by auto
qed
text‹The consequence is that invariants hold in all valid runs.›
lemma invariantsHoldInValidRuns:
fixes F0 :: Formula and decisionVars :: "Variable set"
assumes "invariantsHoldInState stateA F0 decisionVars" and
"(stateA, stateB) ∈ transitionRelation decisionVars"
shows "invariantsHoldInState stateB F0 decisionVars"
using assms
using transitionsPreserveInvariants
using rtrancl_induct[of "stateA" "stateB"
"{(stateA, stateB). transition stateA stateB decisionVars}" "λ x. invariantsHoldInState x F0 decisionVars"]
unfolding transitionRelation_def
by auto
lemma invariantsHoldInValidRunsFromInitialState:
fixes F0 :: Formula and decisionVars :: "Variable set"
assumes "isInitialState state0 F0"
and "(state0, state) ∈ transitionRelation decisionVars"
shows "invariantsHoldInState state F0 decisionVars"
proof-
from ‹isInitialState state0 F0›
have "invariantsHoldInState state0 F0 decisionVars"
by (simp add:invariantsHoldInInitialState)
with assms
show ?thesis
using invariantsHoldInValidRuns [of "state0" "F0" "decisionVars" "state"]
by simp
qed
text‹
In the following text we will show that there are two kinds of states:
\begin{enumerate}
\item \textit{UNSAT} states where @{term "formulaFalse F0 (elements (getM state))"}
and @{term "decisions (getM state) = []"}.
\item \textit{SAT} states where @{term "¬ formulaFalse F0 (elements (getM state))"}
and @{term "vars (elements (getM state)) ⊇ decisionVars"}
\end{enumerate}
The soundness theorems claim that if \textit{UNSAT} state is reached
the formula is unsatisfiable and if \textit{SAT} state is reached,
the formula is satisfiable.
Completeness theorems claim that every final state is either
\textit{UNSAT} or \textit{SAT}. A consequence of this and soundness
theorems, is that if formula is unsatisfiable the solver will finish
in an \textit{UNSAT} state, and if the formula is satisfiable the
solver will finish in a \textit{SAT} state.›
subsection‹Soundness›
theorem soundnessForUNSAT:
fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
assumes
"isInitialState state0 F0" and
"(state0, state) ∈ transitionRelation decisionVars"
"formulaFalse (getF state) (elements (getM state))"
"decisions (getM state) = []"
shows "¬ satisfiable F0"
proof-
from ‹isInitialState state0 F0› ‹(state0, state) ∈ transitionRelation decisionVars›
have "invariantsHoldInState state F0 decisionVars"
using invariantsHoldInValidRunsFromInitialState
by simp
hence "InvariantImpliedLiterals (getF state) (getM state)" "InvariantEquivalent F0 (getF state)"
unfolding invariantsHoldInState_def
by auto
with ‹formulaFalse (getF state) (elements (getM state))›
‹decisions (getM state) = []›
show ?thesis
using unsatReport[of "getF state" "getM state" "F0"]
by simp
qed
theorem soundnessForSAT:
fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
assumes
"vars F0 ⊆ decisionVars" and
"isInitialState state0 F0" and
"(state0, state) ∈ transitionRelation decisionVars"
"¬ formulaFalse (getF state) (elements (getM state))"
"vars (elements (getM state)) ⊇ decisionVars"
shows
"model (elements (getM state)) F0"
proof-
from ‹isInitialState state0 F0› ‹(state0, state) ∈ transitionRelation decisionVars›
have "invariantsHoldInState state F0 decisionVars"
using invariantsHoldInValidRunsFromInitialState
by simp
hence
"InvariantConsistent (getM state)"
"InvariantEquivalent F0 (getF state)"
"InvariantVarsF (getF state) F0 decisionVars"
unfolding invariantsHoldInState_def
by auto
with assms
show ?thesis
using satReport[of "F0" "decisionVars" "getF state" "getM state"]
by simp
qed
subsection‹Termination›
text‹This system is terminating, but only under assumption that
there is no infinite derivation consisting only of applications of
rule $Learn$. We will formalize this condition by requiring that there
there exists an ordering @{term learnL} on the formulae that is
well-founded such that the state is decreased with each application
of the $Learn$ rule. If such ordering exists, the termination
ordering is built as a lexicographic combination of @{term lexLessRestricted}
trail ordering and the @{term learnL} ordering.
›
definition "lexLessState F0 decisionVars == {((stateA::State), (stateB::State)).
(getM stateA, getM stateB) ∈ lexLessRestricted (vars F0 ∪ decisionVars)}"
definition "learnLessState learnL == {((stateA::State), (stateB::State)).
getM stateA = getM stateB ∧ (getF stateA, getF stateB) ∈ learnL}"
definition "terminationLess F0 decisionVars learnL ==
{((stateA::State), (stateB::State)).
(stateA,stateB) ∈ lexLessState F0 decisionVars ∨
(stateA,stateB) ∈ learnLessState learnL}"
text‹We want to show that every valid transition decreases a state
with respect to the constructed termination ordering. Therefore, we
show that $Decide$, $UnitPropagate$ and $Backjump$ rule decrease the
trail with respect to the restricted trail ordering @{term
lexLessRestricted}. Invariants ensure that trails are indeed uniq,
consistent and with finite variable sets. By assumption, $Learn$
rule will decrease the formula component of the state with respect
to the @{term learnL} ordering.›
lemma trailIsDecreasedByDeciedUnitPropagateAndBackjump:
fixes stateA::State and stateB::State
assumes "invariantsHoldInState stateA F0 decisionVars" and
"appliedDecide stateA stateB decisionVars ∨ appliedUnitPropagate stateA stateB ∨ appliedBackjump stateA stateB"
shows "(getM stateB, getM stateA) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
proof-
from ‹appliedDecide stateA stateB decisionVars ∨ appliedUnitPropagate stateA stateB ∨ appliedBackjump stateA stateB›
‹invariantsHoldInState stateA F0 decisionVars›
have "invariantsHoldInState stateB F0 decisionVars"
using transitionsPreserveInvariants
unfolding transition_def
by auto
from ‹invariantsHoldInState stateA F0 decisionVars›
have *: "uniq (elements (getM stateA))" "consistent (elements (getM stateA))" "vars (elements (getM stateA)) ⊆ vars F0 ∪ decisionVars"
unfolding invariantsHoldInState_def
unfolding InvariantVarsM_def
unfolding InvariantConsistent_def
unfolding InvariantUniq_def
by auto
from ‹invariantsHoldInState stateB F0 decisionVars›
have **: "uniq (elements (getM stateB))" "consistent (elements (getM stateB))" "vars (elements (getM stateB)) ⊆ vars F0 ∪ decisionVars"
unfolding invariantsHoldInState_def
unfolding InvariantVarsM_def
unfolding InvariantConsistent_def
unfolding InvariantUniq_def
by auto
{
assume "appliedDecide stateA stateB decisionVars"
hence "(getM stateB, getM stateA) ∈ lexLess"
unfolding appliedDecide_def
by (auto simp add:lexLessAppend)
with * **
have "((getM stateB), (getM stateA)) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
unfolding lexLessRestricted_def
by auto
}
moreover
{
assume "appliedUnitPropagate stateA stateB"
hence "(getM stateB, getM stateA) ∈ lexLess"
unfolding appliedUnitPropagate_def
by (auto simp add:lexLessAppend)
with * **
have "(getM stateB, getM stateA) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
unfolding lexLessRestricted_def
by auto
}
moreover
{
assume "appliedBackjump stateA stateB"
then obtain bc::Clause and bl::Literal and level::nat
where
"isUnitClause bc bl (elements (prefixToLevel level (getM stateA)))"
"formulaEntailsClause (getF stateA) bc"
"var bl ∈ vars (getF stateA) ∪ vars (elements (getM stateA))"
"0 ≤ level" "level < currentLevel (getM stateA)"
"getF stateB = getF stateA"
"getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]"
unfolding appliedBackjump_def
by auto
with ‹getM stateB = prefixToLevel level (getM stateA) @ [(bl, False)]›
have "(getM stateB, getM stateA) ∈ lexLess"
by (simp add:lexLessBackjump)
with * **
have "(getM stateB, getM stateA) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
unfolding lexLessRestricted_def
by auto
}
ultimately
show ?thesis
using assms
by auto
qed
text‹Now we can show that, under the assumption for $Learn$ rule,
every rule application decreases a state with respect to the
constructed termination ordering.›
theorem stateIsDecreasedByValidTransitions:
fixes stateA::State and stateB::State
assumes "invariantsHoldInState stateA F0 decisionVars" and "transition stateA stateB decisionVars"
"appliedLearn stateA stateB ⟶ (getF stateB, getF stateA) ∈ learnL"
shows "(stateB, stateA) ∈ terminationLess F0 decisionVars learnL"
proof-
{
assume "appliedDecide stateA stateB decisionVars ∨ appliedUnitPropagate stateA stateB ∨ appliedBackjump stateA stateB"
with ‹invariantsHoldInState stateA F0 decisionVars›
have "(getM stateB, getM stateA) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
using trailIsDecreasedByDeciedUnitPropagateAndBackjump
by simp
hence "(stateB, stateA) ∈ lexLessState F0 decisionVars"
unfolding lexLessState_def
by simp
hence "(stateB, stateA) ∈ terminationLess F0 decisionVars learnL"
unfolding terminationLess_def
by simp
}
moreover
{
assume "appliedLearn stateA stateB"
with ‹appliedLearn stateA stateB ⟶ (getF stateB, getF stateA) ∈ learnL›
have "(getF stateB, getF stateA) ∈ learnL"
by simp
moreover
from ‹appliedLearn stateA stateB›
have "(getM stateB) = (getM stateA)"
unfolding appliedLearn_def
by auto
ultimately
have "(stateB, stateA) ∈ learnLessState learnL"
unfolding learnLessState_def
by simp
hence "(stateB, stateA) ∈ terminationLess F0 decisionVars learnL"
unfolding terminationLess_def
by simp
}
ultimately
show ?thesis
using ‹transition stateA stateB decisionVars›
unfolding transition_def
by auto
qed
text‹The minimal states with respect to the termination ordering are
final i.e., no further transition rules are applicable.›
definition
"isMinimalState stateMin F0 decisionVars learnL == (∀ state::State. (state, stateMin) ∉ terminationLess F0 decisionVars learnL)"
lemma minimalStatesAreFinal:
fixes stateA::State
assumes *: "∀ (stateA::State) (stateB::State). appliedLearn stateA stateB ⟶ (getF stateB, getF stateA) ∈ learnL" and
"invariantsHoldInState state F0 decisionVars" and "isMinimalState state F0 decisionVars learnL"
shows "isFinalState state decisionVars"
proof-
{
assume "¬ ?thesis"
then obtain state'::State
where "transition state state' decisionVars"
unfolding isFinalState_def
by auto
with ‹invariantsHoldInState state F0 decisionVars› *
have "(state', state) ∈ terminationLess F0 decisionVars learnL"
using stateIsDecreasedByValidTransitions[of "state" "F0" "decisionVars" "state'" "learnL"]
unfolding transition_def
by auto
with ‹isMinimalState state F0 decisionVars learnL›
have False
unfolding isMinimalState_def
by auto
}
thus ?thesis
by auto
qed
text‹We now prove that termination ordering is well founded. We
start with two auxiliary lemmas.›
lemma wfLexLessState:
fixes decisionVars :: "Variable set" and F0 :: "Formula"
assumes "finite decisionVars"
shows "wf (lexLessState F0 decisionVars)"
unfolding wf_eq_minimal
proof-
show "∀Q state. state ∈ Q ⟶ (∃stateMin∈Q. ∀state'. (state', stateMin) ∈ lexLessState F0 decisionVars ⟶ state' ∉ Q)"
proof-
{
fix Q :: "State set" and state :: State
assume "state ∈ Q"
let ?Q1 = "{M::LiteralTrail. ∃ state. state ∈ Q ∧ (getM state) = M}"
from ‹state ∈ Q›
have "getM state ∈ ?Q1"
by auto
from ‹finite decisionVars›
have "finite (vars F0 ∪ decisionVars)"
using finiteVarsFormula[of "F0"]
by simp
hence "wf (lexLessRestricted (vars F0 ∪ decisionVars))"
using wfLexLessRestricted[of "vars F0 ∪ decisionVars"]
by simp
with ‹getM state ∈ ?Q1›
obtain Mmin where "Mmin ∈ ?Q1" "∀M'. (M', Mmin) ∈ lexLessRestricted (vars F0 ∪ decisionVars) ⟶ M' ∉ ?Q1"
unfolding wf_eq_minimal
apply (erule_tac x="?Q1" in allE)
apply (erule_tac x="getM state" in allE)
by auto
from ‹Mmin ∈ ?Q1› obtain stateMin
where "stateMin ∈ Q" "(getM stateMin) = Mmin"
by auto
have "∀state'. (state', stateMin) ∈ lexLessState F0 decisionVars ⟶ state' ∉ Q"
proof
fix state'
show "(state', stateMin) ∈ lexLessState F0 decisionVars ⟶ state' ∉ Q"
proof
assume "(state', stateMin) ∈ lexLessState F0 decisionVars"
hence "(getM state', getM stateMin) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
unfolding lexLessState_def
by auto
from ‹∀M'. (M', Mmin) ∈ lexLessRestricted (vars F0 ∪ decisionVars) ⟶ M' ∉ ?Q1›
‹(getM state', getM stateMin) ∈ lexLessRestricted (vars F0 ∪ decisionVars)› ‹getM stateMin = Mmin›
have "getM state' ∉ ?Q1"
by simp
with ‹getM stateMin = Mmin›
show "state' ∉ Q"
by auto
qed
qed
with ‹stateMin ∈ Q›
have "∃ stateMin ∈ Q. (∀state'. (state', stateMin) ∈ lexLessState F0 decisionVars ⟶ state' ∉ Q)"
by auto
}
thus ?thesis
by auto
qed
qed
lemma wfLearnLessState:
assumes "wf learnL"
shows "wf (learnLessState learnL)"
unfolding wf_eq_minimal
proof-
show "∀Q state. state ∈ Q ⟶ (∃stateMin∈Q. ∀state'. (state', stateMin) ∈ learnLessState learnL ⟶ state' ∉ Q)"
proof-
{
fix Q :: "State set" and state :: State
assume "state ∈ Q"
let ?M = "(getM state)"
let ?Q1 = "{f::Formula. ∃ state. state ∈ Q ∧ (getM state) = ?M ∧ (getF state) = f}"
from ‹state ∈ Q›
have "getF state ∈ ?Q1"
by auto
with ‹wf learnL›
obtain FMin where "FMin ∈ ?Q1" "∀F'. (F', FMin) ∈ learnL ⟶ F' ∉ ?Q1"
unfolding wf_eq_minimal
apply (erule_tac x="?Q1" in allE)
apply (erule_tac x="getF state" in allE)
by auto
from ‹FMin ∈ ?Q1› obtain stateMin
where "stateMin ∈ Q" "(getM stateMin) = ?M" "getF stateMin = FMin"
by auto
have "∀state'. (state', stateMin) ∈ learnLessState learnL ⟶ state' ∉ Q"
proof
fix state'
show "(state', stateMin) ∈ learnLessState learnL ⟶ state' ∉ Q"
proof
assume "(state', stateMin) ∈ learnLessState learnL"
with ‹getM stateMin = ?M›
have "getM state' = getM stateMin" "(getF state', getF stateMin) ∈ learnL"
unfolding learnLessState_def
by auto
from ‹∀F'. (F', FMin) ∈ learnL ⟶ F' ∉ ?Q1›
‹(getF state', getF stateMin) ∈ learnL› ‹getF stateMin = FMin›
have "getF state' ∉ ?Q1"
by simp
with ‹getM state' = getM stateMin› ‹getM stateMin = ?M›
show "state' ∉ Q"
by auto
qed
qed
with ‹stateMin ∈ Q›
have "∃ stateMin ∈ Q. (∀state'. (state', stateMin) ∈ learnLessState learnL ⟶ state' ∉ Q)"
by auto
}
thus ?thesis
by auto
qed
qed
text‹Now we can prove the following key lemma which shows that the
termination ordering is well founded.›
lemma wfTerminationLess:
fixes F0 :: Formula and decisionVars :: "Variable set"
assumes "finite decisionVars" "wf learnL"
shows "wf (terminationLess F0 decisionVars learnL)"
unfolding wf_eq_minimal
proof-
show "∀Q state. state ∈ Q ⟶ (∃ stateMin ∈ Q. ∀state'. (state', stateMin) ∈ terminationLess F0 decisionVars learnL ⟶ state' ∉ Q)"
proof-
{
fix Q::"State set"
fix state::State
assume "state ∈ Q"
have "wf (lexLessState F0 decisionVars)"
using wfLexLessState[of "decisionVars" "F0"]
using ‹finite decisionVars›
by simp
with ‹state ∈ Q› obtain state0
where "state0 ∈ Q" "∀state'. (state', state0) ∈ lexLessState F0 decisionVars ⟶ state' ∉ Q"
unfolding wf_eq_minimal
by auto
let ?Q0 = "{state. state ∈ Q ∧ (getM state) = (getM state0)}"
from ‹state0 ∈ Q›
have "state0 ∈ ?Q0"
by simp
from ‹wf learnL›
have "wf (learnLessState learnL)"
using wfLearnLessState
by simp
with ‹state0 ∈ ?Q0› obtain state1
where "state1 ∈ ?Q0" "∀state'. (state', state1) ∈ learnLessState learnL ⟶ state' ∉ ?Q0"
unfolding wf_eq_minimal
apply (erule_tac x="?Q0" in allE)
apply (erule_tac x="state0" in allE)
by auto
from ‹state1 ∈ ?Q0›
have "state1 ∈ Q" "getM state1 = getM state0"
by auto
let ?stateMin = state1
have "∀state'. (state', ?stateMin) ∈ terminationLess F0 decisionVars learnL ⟶ state' ∉ Q"
proof
fix state'
show "(state', ?stateMin) ∈ terminationLess F0 decisionVars learnL ⟶ state' ∉ Q"
proof
assume "(state', ?stateMin) ∈ terminationLess F0 decisionVars learnL"
hence
"(state', ?stateMin) ∈ lexLessState F0 decisionVars ∨
(state', ?stateMin) ∈ learnLessState learnL"
unfolding terminationLess_def
by auto
moreover
{
assume "(state', ?stateMin) ∈ lexLessState F0 decisionVars"
with ‹getM state1 = getM state0›
have "(state', state0) ∈ lexLessState F0 decisionVars"
unfolding lexLessState_def
by simp
with ‹∀state'. (state', state0) ∈ lexLessState F0 decisionVars ⟶ state' ∉ Q›
have "state' ∉ Q"
by simp
}
moreover
{
assume "(state', ?stateMin) ∈ learnLessState learnL"
with ‹∀state'. (state', state1) ∈ learnLessState learnL ⟶ state' ∉ ?Q0›
have "state' ∉ ?Q0"
by simp
from ‹(state', state1) ∈ learnLessState learnL› ‹getM state1 = getM state0›
have "getM state' = getM state0"
unfolding learnLessState_def
by auto
with ‹state' ∉ ?Q0›
have "state' ∉ Q"
by simp
}
ultimately
show "state' ∉ Q"
by auto
qed
qed
with ‹?stateMin ∈ Q› have "(∃ stateMin ∈ Q. ∀state'. (state', stateMin) ∈ terminationLess F0 decisionVars learnL ⟶ state' ∉ Q)"
by auto
}
thus ?thesis
by simp
qed
qed
text‹Using the termination ordering we show that the transition
relation is well founded on states reachable from initial state. The
assumption for the $Learn$ rule is neccessary.›
theorem wfTransitionRelation:
fixes decisionVars :: "Variable set" and F0 :: "Formula"
assumes "finite decisionVars" and "isInitialState state0 F0" and
*: "∃ learnL::(Formula × Formula) set.
wf learnL ∧
(∀ stateA stateB. appliedLearn stateA stateB ⟶ (getF stateB, getF stateA) ∈ learnL)"
shows "wf {(stateB, stateA).
(state0, stateA) ∈ transitionRelation decisionVars ∧ (transition stateA stateB decisionVars)}"
proof-
from * obtain learnL::"(Formula × Formula) set"
where
"wf learnL" and
**: "∀ stateA stateB. appliedLearn stateA stateB ⟶ (getF stateB, getF stateA) ∈ learnL"
by auto
let ?rel = "{(stateB, stateA).
(state0, stateA) ∈ transitionRelation decisionVars ∧ (transition stateA stateB decisionVars)}"
let ?rel'= "terminationLess F0 decisionVars learnL"
have "∀x y. (x, y) ∈ ?rel ⟶ (x, y) ∈ ?rel'"
proof-
{
fix stateA::State and stateB::State
assume "(stateB, stateA) ∈ ?rel"
hence "(stateB, stateA) ∈ ?rel'"
using ‹isInitialState state0 F0›
using invariantsHoldInValidRunsFromInitialState[of "state0" "F0" "stateA" "decisionVars"]
using stateIsDecreasedByValidTransitions[of "stateA" "F0" "decisionVars" "stateB"] **
by simp
}
thus ?thesis
by simp
qed
moreover
have "wf ?rel'"
using ‹finite decisionVars› ‹wf learnL›
by (rule wfTerminationLess)
ultimately
show ?thesis
using wellFoundedEmbed[of "?rel" "?rel'"]
by simp
qed
text‹We will now give two corollaries of the previous theorem. First
is a weak termination result that shows that there is a terminating
run from every intial state to the final one.›
corollary
fixes decisionVars :: "Variable set" and F0 :: "Formula" and state0 :: "State"
assumes "finite decisionVars" and "isInitialState state0 F0" and
*: "∃ learnL::(Formula × Formula) set.
wf learnL ∧
(∀ stateA stateB. appliedLearn stateA stateB ⟶ (getF stateB, getF stateA) ∈ learnL)"
shows "∃ state. (state0, state) ∈ transitionRelation decisionVars ∧ isFinalState state decisionVars"
proof-
{
assume "¬ ?thesis"
let ?Q = "{state. (state0, state) ∈ transitionRelation decisionVars}"
let ?rel = "{(stateB, stateA). (state0, stateA) ∈ transitionRelation decisionVars ∧
transition stateA stateB decisionVars}"
have "state0 ∈ ?Q"
unfolding transitionRelation_def
by simp
hence "∃ state. state ∈ ?Q"
by auto
from assms
have "wf ?rel"
using wfTransitionRelation[of "decisionVars" "state0" "F0"]
by auto
hence "∀ Q. (∃ x. x ∈ Q) ⟶ (∃ stateMin ∈ Q. ∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ Q)"
unfolding wf_eq_minimal
by simp
hence " (∃ x. x ∈ ?Q) ⟶ (∃ stateMin ∈ ?Q. ∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ ?Q)"
by rule
with ‹∃ state. state ∈ ?Q›
have "∃ stateMin ∈ ?Q. ∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ ?Q"
by simp
then obtain stateMin
where "stateMin ∈ ?Q" and "∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ ?Q"
by auto
from ‹stateMin ∈ ?Q›
have "(state0, stateMin) ∈ transitionRelation decisionVars"
by simp
with ‹¬ ?thesis›
have "¬ isFinalState stateMin decisionVars"
by simp
then obtain state'::State
where "transition stateMin state' decisionVars"
unfolding isFinalState_def
by auto
have "(state', stateMin) ∈ ?rel"
using ‹(state0, stateMin) ∈ transitionRelation decisionVars›
‹transition stateMin state' decisionVars›
by simp
with ‹∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ ?Q›
have "state' ∉ ?Q"
by force
moreover
from ‹(state0, stateMin) ∈ transitionRelation decisionVars› ‹transition stateMin state' decisionVars›
have "state' ∈ ?Q"
unfolding transitionRelation_def
using rtrancl_into_rtrancl[of "state0" "stateMin" "{(stateA, stateB). transition stateA stateB decisionVars}" "state'"]
by simp
ultimately
have False
by simp
}
thus ?thesis
by auto
qed
text‹Now we prove the final strong termination result which states
that there cannot be infinite chains of transitions. If there is an
infinite transition chain that starts from an initial state, its
elements would for a set that would contain initial state and for
every element of that set there would be another element of that set
that is directly reachable from it. We show that no such set exists.›
corollary noInfiniteTransitionChains:
fixes F0::Formula and decisionVars::"Variable set"
assumes "finite decisionVars" and
*: "∃ learnL::(Formula × Formula) set.
wf learnL ∧
(∀ stateA stateB. appliedLearn stateA stateB ⟶ (getF stateB, getF stateA) ∈ learnL)"
shows "¬ (∃ Q::(State set). ∃ state0 ∈ Q. isInitialState state0 F0 ∧
(∀ state ∈ Q. (∃ state' ∈ Q. transition state state' decisionVars))
)"
proof-
{
assume "¬ ?thesis"
then obtain Q::"State set" and state0::"State"
where "isInitialState state0 F0" "state0 ∈ Q"
"∀ state ∈ Q. (∃ state' ∈ Q. transition state state' decisionVars)"
by auto
let ?rel = "{(stateB, stateA). (state0, stateA) ∈ transitionRelation decisionVars ∧
transition stateA stateB decisionVars}"
from ‹finite decisionVars› ‹isInitialState state0 F0› *
have "wf ?rel"
using wfTransitionRelation
by simp
hence wfmin: "∀Q x. x ∈ Q ⟶
(∃z∈Q. ∀y. (y, z) ∈ ?rel ⟶ y ∉ Q)"
unfolding wf_eq_minimal
by simp
let ?Q = "{state ∈ Q. (state0, state) ∈ transitionRelation decisionVars}"
from ‹state0 ∈ Q›
have "state0 ∈ ?Q"
unfolding transitionRelation_def
by simp
with wfmin
obtain stateMin::State
where "stateMin ∈ ?Q" and "∀y. (y, stateMin) ∈ ?rel ⟶ y ∉ ?Q"
apply (erule_tac x="?Q" in allE)
by auto
from ‹stateMin ∈ ?Q›
have "stateMin ∈ Q" "(state0, stateMin) ∈ transitionRelation decisionVars"
by auto
with ‹∀ state ∈ Q. (∃ state' ∈ Q. transition state state' decisionVars)›
obtain state'::State
where "state' ∈ Q" "transition stateMin state' decisionVars"
by auto
with ‹(state0, stateMin) ∈ transitionRelation decisionVars›
have "(state', stateMin) ∈ ?rel"
by simp
with ‹∀y. (y, stateMin) ∈ ?rel ⟶ y ∉ ?Q›
have "state' ∉ ?Q"
by force
from ‹state' ∈ Q› ‹(state0, stateMin) ∈ transitionRelation decisionVars›
‹transition stateMin state' decisionVars›
have "state' ∈ ?Q"
unfolding transitionRelation_def
using rtrancl_into_rtrancl[of "state0" "stateMin" "{(stateA, stateB). transition stateA stateB decisionVars}" "state'"]
by simp
with ‹state' ∉ ?Q›
have False
by simp
}
thus ?thesis
by force
qed
subsection‹Completeness›
text‹In this section we will first show that each final state is
either \textit{SAT} or \textit{UNSAT} state.›
lemma finalNonConflictState:
fixes state::State and FO :: Formula
assumes
"¬ applicableDecide state decisionVars"
shows "vars (elements (getM state)) ⊇ decisionVars"
proof
fix x :: Variable
let ?l = "Pos x"
assume "x ∈ decisionVars"
hence "var ?l = x" and "var ?l ∈ decisionVars" and "var (opposite ?l) ∈ decisionVars"
by auto
with ‹¬ applicableDecide state decisionVars›
have "literalTrue ?l (elements (getM state)) ∨ literalFalse ?l (elements (getM state))"
unfolding applicableDecideCharacterization
by force
with ‹var ?l = x›
show "x ∈ vars (elements (getM state))"
using valuationContainsItsLiteralsVariable[of "?l" "elements (getM state)"]
using valuationContainsItsLiteralsVariable[of "opposite ?l" "elements (getM state)"]
by auto
qed
lemma finalConflictingState:
fixes state :: State
assumes
"InvariantUniq (getM state)" and
"InvariantConsistent (getM state)" and
"InvariantImpliedLiterals (getF state) (getM state)"
"¬ applicableBackjump state" and
"formulaFalse (getF state) (elements (getM state))"
shows
"decisions (getM state) = []"
proof-
from ‹InvariantUniq (getM state)›
have "uniq (elements (getM state))"
unfolding InvariantUniq_def
.
from ‹InvariantConsistent (getM state)›
have "consistent (elements (getM state))"
unfolding InvariantConsistent_def
.
let ?c = "oppositeLiteralList (decisions (getM state))"
{
assume "¬ ?thesis"
hence "?c ≠ []"
using oppositeLiteralListNonempty[of "decisions (getM state)"]
by simp
moreover
have "clauseFalse ?c (elements (getM state))"
proof-
{
fix l::Literal
assume "l el ?c"
hence "opposite l el decisions (getM state)"
using literalElListIffOppositeLiteralElOppositeLiteralList [of "l" "?c"]
by simp
hence "literalFalse l (elements (getM state))"
using markedElementsAreElements[of "opposite l" "getM state"]
by simp
}
thus ?thesis
using clauseFalseIffAllLiteralsAreFalse[of "?c" "elements (getM state)"]
by simp
qed
moreover
let ?l = "getLastAssertedLiteral (oppositeLiteralList ?c) (elements (getM state))"
have "isLastAssertedLiteral ?l (oppositeLiteralList ?c) (elements (getM state))"
using ‹InvariantUniq (getM state)›
using getLastAssertedLiteralCharacterization[of "?c" "elements (getM state)"]
‹?c ≠ []› ‹clauseFalse ?c (elements (getM state))›
unfolding InvariantUniq_def
by simp
moreover
have "∀ l. l el ?c ⟶ (opposite l) el (decisions (getM state))"
proof-
{
fix l::Literal
assume "l el ?c"
hence "(opposite l) el (oppositeLiteralList ?c)"
using literalElListIffOppositeLiteralElOppositeLiteralList[of "l" "?c"]
by simp
}
thus ?thesis
by simp
qed
ultimately
have "∃ level. (isBackjumpLevel level (opposite ?l) ?c (getM state))"
using ‹uniq (elements (getM state))›
using allDecisionsThenExistsBackjumpLevel[of "getM state" "?c" "opposite ?l"]
by simp
then obtain level::nat
where "isBackjumpLevel level (opposite ?l) ?c (getM state)"
by auto
with ‹consistent (elements (getM state))› ‹uniq (elements (getM state))› ‹clauseFalse ?c (elements (getM state))›
have "isUnitClause ?c (opposite ?l) (elements (prefixToLevel level (getM state)))"
using isBackjumpLevelEnsuresIsUnitInPrefix[of "getM state" "?c" "level" "opposite ?l"]
by simp
moreover
have "formulaEntailsClause (getF state) ?c"
proof-
from ‹clauseFalse ?c (elements (getM state))› ‹consistent (elements (getM state))›
have "¬ clauseTautology ?c"
using tautologyNotFalse[of "?c" "elements (getM state)"]
by auto
from ‹formulaFalse (getF state) (elements (getM state))› ‹InvariantImpliedLiterals (getF state) (getM state)›
have "¬ satisfiable ((getF state) @ val2form (decisions (getM state)))"
using InvariantImpliedLiteralsAndFormulaFalseThenFormulaAndDecisionsAreNotSatisfiable
by simp
hence "¬ satisfiable ((getF state) @ val2form (oppositeLiteralList ?c))"
by simp
with ‹¬ clauseTautology ?c›
show ?thesis
using unsatisfiableFormulaWithSingleLiteralClauses
by simp
qed
moreover
have "var ?l ∈ vars (getF state) ∪ vars (elements (getM state))"
proof-
from ‹isLastAssertedLiteral ?l (oppositeLiteralList ?c) (elements (getM state))›
have "?l el (oppositeLiteralList ?c)"
unfolding isLastAssertedLiteral_def
by simp
hence "literalTrue ?l (elements (getM state))"
by (simp add: markedElementsAreElements)
hence "var ?l ∈ vars (elements (getM state))"
using valuationContainsItsLiteralsVariable[of "?l" "elements (getM state)"]
by simp
thus ?thesis
by simp
qed
moreover
have "0 ≤ level" "level < (currentLevel (getM state))"
proof-
from ‹isBackjumpLevel level (opposite ?l) ?c (getM state)›
have "0 ≤ level" "level < (elementLevel ?l (getM state))"
unfolding isBackjumpLevel_def
by auto
thus "0 ≤ level" "level < (currentLevel (getM state))"
using elementLevelLeqCurrentLevel[of "?l" "getM state"]
by auto
qed
ultimately
have "applicableBackjump state"
unfolding applicableBackjumpCharacterization
by force
with ‹¬ applicableBackjump state›
have "False"
by simp
}
thus ?thesis
by auto
qed
lemma finalStateCharacterizationLemma:
fixes state :: State
assumes
"InvariantUniq (getM state)" and
"InvariantConsistent (getM state)" and
"InvariantImpliedLiterals (getF state) (getM state)"
"¬ applicableDecide state decisionVars" and
"¬ applicableBackjump state"
shows
"(¬ formulaFalse (getF state) (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars) ∨
(formulaFalse (getF state) (elements (getM state)) ∧ decisions (getM state) = [])"
proof (cases "formulaFalse (getF state) (elements (getM state))")
case True
hence "decisions (getM state) = []"
using assms
using finalConflictingState
by auto
with True
show ?thesis
by simp
next
case False
hence "vars (elements (getM state)) ⊇ decisionVars"
using assms
using finalNonConflictState
by auto
with False
show ?thesis
by simp
qed
theorem finalStateCharacterization:
fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
assumes
"isInitialState state0 F0" and
"(state0, state) ∈ transitionRelation decisionVars" and
"isFinalState state decisionVars"
shows
"(¬ formulaFalse (getF state) (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars) ∨
(formulaFalse (getF state) (elements (getM state)) ∧ decisions (getM state) = [])"
proof-
from ‹isInitialState state0 F0› ‹(state0, state) ∈ transitionRelation decisionVars›
have "invariantsHoldInState state F0 decisionVars"
using invariantsHoldInValidRunsFromInitialState
by simp
hence
*: "InvariantUniq (getM state)"
"InvariantConsistent (getM state)"
"InvariantImpliedLiterals (getF state) (getM state)"
unfolding invariantsHoldInState_def
by auto
from ‹isFinalState state decisionVars›
have **:
"¬ applicableBackjump state"
"¬ applicableDecide state decisionVars"
unfolding finalStateNonApplicable
by auto
from * **
show ?thesis
using finalStateCharacterizationLemma[of "state" "decisionVars"]
by simp
qed
text‹Completeness theorems are easy consequences of this characterization and
soundness.›
theorem completenessForSAT:
fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
assumes
"satisfiable F0" and
"isInitialState state0 F0" and
"(state0, state) ∈ transitionRelation decisionVars" and
"isFinalState state decisionVars"
shows "¬ formulaFalse (getF state) (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars"
proof-
from assms
have *: "(¬ formulaFalse (getF state) (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars) ∨
(formulaFalse (getF state) (elements (getM state)) ∧ decisions (getM state) = [])"
using finalStateCharacterization[of "state0" "F0" "state" "decisionVars"]
by auto
{
assume "formulaFalse (getF state) (elements (getM state))"
with *
have "formulaFalse (getF state) (elements (getM state))" "decisions (getM state) = []"
by auto
with assms
have "¬ satisfiable F0"
using soundnessForUNSAT
by simp
with ‹satisfiable F0›
have False
by simp
}
with * show ?thesis
by auto
qed
theorem completenessForUNSAT:
fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
assumes
"vars F0 ⊆ decisionVars" and
"¬ satisfiable F0" and
"isInitialState state0 F0" and
"(state0, state) ∈ transitionRelation decisionVars" and
"isFinalState state decisionVars"
shows
"formulaFalse (getF state) (elements (getM state)) ∧ decisions (getM state) = []"
proof-
from assms
have *:
"(¬ formulaFalse (getF state) (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars) ∨
(formulaFalse (getF state) (elements (getM state)) ∧ decisions (getM state) = [])"
using finalStateCharacterization[of "state0" "F0" "state" "decisionVars"]
by auto
{
assume "¬ formulaFalse (getF state) (elements (getM state))"
with *
have "¬ formulaFalse (getF state) (elements (getM state))" "vars (elements (getM state)) ⊇ decisionVars"
by auto
with assms
have "satisfiable F0"
using soundnessForSAT[of "F0" "decisionVars" "state0" "state"]
unfolding satisfiable_def
by auto
with ‹¬ satisfiable F0›
have False
by simp
}
with * show ?thesis
by auto
qed
theorem partialCorrectness:
fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
assumes
"vars F0 ⊆ decisionVars" and
"isInitialState state0 F0" and
"(state0, state) ∈ transitionRelation decisionVars" and
"isFinalState state decisionVars"
shows
"satisfiable F0 = (¬ formulaFalse (getF state) (elements (getM state)))"
using assms
using completenessForUNSAT[of "F0" "decisionVars" "state0" "state"]
using completenessForSAT[of "F0" "state0" "state" "decisionVars"]
by auto
end