Theory SAT_Solve_SAS_Plus
theory SAT_Solve_SAS_Plus
imports "SAS_Plus_STRIPS"
"SAT_Plan_Extensions"
begin
section "SAT-Solving of SAS+ Problems"
lemma sas_plus_problem_has_serial_solution_iff_i:
assumes "is_valid_problem_sas_plus Ψ"
and "𝒜 ⊨ Φ⇩∀ (φ Ψ) t"
shows "is_serial_solution_for_problem Ψ [φ⇩O¯ Ψ op. op ← concat (Φ¯ (φ Ψ) 𝒜 t)]"
proof -
let ?Π = "φ Ψ"
and ?π' = "concat (Φ¯ (φ Ψ) 𝒜 t)"
let ?ψ = "[φ⇩O¯ Ψ op. op ← ?π']"
{
have "is_valid_problem_strips ?Π"
using is_valid_problem_sas_plus_then_strips_transformation_too[OF assms(1)].
moreover have "STRIPS_Semantics.is_serial_solution_for_problem ?Π ?π'"
using calculation serializable_encoding_decoded_plan_is_serializable[OF
_ assms(2)]
unfolding decode_plan_def
by simp
ultimately have "SAS_Plus_Semantics.is_serial_solution_for_problem Ψ ?ψ"
using assms(1) serial_strips_equivalent_to_serial_sas_plus
by blast
}
thus ?thesis
using serial_strips_equivalent_to_serial_sas_plus[OF assms(1)]
by blast
qed
lemma sas_plus_problem_has_serial_solution_iff_ii:
assumes "is_valid_problem_sas_plus Ψ"
and "is_serial_solution_for_problem Ψ ψ"
and "h = length ψ"
shows "∃𝒜. (𝒜 ⊨ Φ⇩∀ (φ Ψ) h)"
proof -
let ?Π = "φ Ψ"
and ?π = "φ⇩P Ψ (embed ψ)"
let ?𝒜 = "valuation_for_plan ?Π ?π"
let ?t = "length ψ"
have nb: "length ψ = length ?π"
unfolding SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def
sasp_op_to_strips_def
sas_plus_parallel_plan_to_strips_parallel_plan_def
by (induction ψ; auto)
have "is_valid_problem_strips ?Π"
using assms(1) is_valid_problem_sas_plus_then_strips_transformation_too
by blast
moreover have "STRIPS_Semantics.is_parallel_solution_for_problem ?Π ?π"
using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus[OF assms(1,2)]
strips_equivalent_to_sas_plus[OF assms(1)]
by blast
moreover {
fix k
assume "k < length ?π"
moreover obtain ops' where "ops' = ?π ! k"
by simp
moreover have "ops' ∈ set ?π"
using calculation nth_mem
by blast
moreover have "?π = [[φ⇩O Ψ op. op ← ops]. ops ← embed ψ]"
unfolding SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def
sasp_op_to_strips_def
sas_plus_parallel_plan_to_strips_parallel_plan_def
..
moreover obtain ops
where "ops' = [φ⇩O Ψ op. op ← ops]"
and "ops ∈ set (embed ψ)"
using calculation(3, 4)
by auto
moreover have "ops ∈ { [op] | op. op ∈ set ψ }"
using calculation(6) set_of_embed_is
by blast
moreover obtain op
where "ops = [op]" and "op ∈ set ψ"
using calculation(7)
by blast
ultimately have "are_all_operators_non_interfering (?π ! k)"
by fastforce
}
ultimately show ?thesis
using encode_problem_serializable_complete nb
by (auto simp: assms(3))
qed
text ‹ To wrap-up our documentation of the Isabelle formalization, we take a look at the central
theorem which combines all the previous theorem to show that SAS+ problems \<^term>‹Ψ› can be solved
using the planning as satisfiability framework.
A solution \<^term>‹ψ› for the SAS+ problem \<^term>‹Ψ› exists if and only if a model \<^term>‹𝒜› and a
hypothesized plan length \<^term>‹t› exist s.t.
@{text[display,indent=4] "𝒜 ⊨ Φ⇩∀ (φ Ψ) t"}
for the serializable SATPlan encoding of the corresponding STRIPS problem \<^term>‹Φ⇩∀ (φ Ψ) t› exist. ›
theorem sas_plus_problem_has_serial_solution_iff:
assumes "is_valid_problem_sas_plus Ψ"
shows "(∃ψ. is_serial_solution_for_problem Ψ ψ) ⟷ (∃𝒜 t. 𝒜 ⊨ Φ⇩∀ (φ Ψ) t)"
using sas_plus_problem_has_serial_solution_iff_i[OF assms]
sas_plus_problem_has_serial_solution_iff_ii[OF assms]
by blast
section ‹Adding Noop actions to the SAS+ problem›
text ‹Here we add noop actions to the SAS+ problem to enable the SAT formula to be satisfiable if
there are plans that are shorter than the given horizons.›
definition "empty_sasp_action ≡ ⦇SAS_Plus_Representation.sas_plus_operator.precondition_of = [],
SAS_Plus_Representation.sas_plus_operator.effect_of = []⦈"
lemma sasp_exec_noops: "execute_serial_plan_sas_plus s (replicate n empty_sasp_action) = s"
by (induction n arbitrary: )
(auto simp: empty_sasp_action_def STRIPS_Representation.is_operator_applicable_in_def
execute_operator_def)
definition
"prob_with_noop Π ≡
⦇SAS_Plus_Representation.sas_plus_problem.variables_of = SAS_Plus_Representation.sas_plus_problem.variables_of Π,
SAS_Plus_Representation.sas_plus_problem.operators_of = empty_sasp_action # SAS_Plus_Representation.sas_plus_problem.operators_of Π,
SAS_Plus_Representation.sas_plus_problem.initial_of = SAS_Plus_Representation.sas_plus_problem.initial_of Π,
SAS_Plus_Representation.sas_plus_problem.goal_of = SAS_Plus_Representation.sas_plus_problem.goal_of Π,
SAS_Plus_Representation.sas_plus_problem.range_of = SAS_Plus_Representation.sas_plus_problem.range_of Π⦈"
lemma sasp_noops_in_noop_problem: "set (replicate n empty_sasp_action) ⊆ set (SAS_Plus_Representation.sas_plus_problem.operators_of (prob_with_noop Π))"
by (induction n) (auto simp: prob_with_noop_def)
lemma noops_complete:
"SAS_Plus_Semantics.is_serial_solution_for_problem Ψ π ⟹
SAS_Plus_Semantics.is_serial_solution_for_problem (prob_with_noop Ψ) ((replicate n empty_sasp_action) @ π)"
by(induction n)
(auto simp: SAS_Plus_Semantics.is_serial_solution_for_problem_def insert list.pred_set
sasp_exec_noops prob_with_noop_def Let_def empty_sasp_action_def elem)
definition "rem_noops ≡ filter (λop. op ≠ empty_sasp_action)"
lemma sasp_filter_empty_action:
"execute_serial_plan_sas_plus s (rem_noops πs) = execute_serial_plan_sas_plus s πs"
by (induction πs arbitrary: s)
(auto simp: empty_sasp_action_def rem_noops_def)
lemma noops_sound:
"SAS_Plus_Semantics.is_serial_solution_for_problem (prob_with_noop Ψ) πs ⟹
SAS_Plus_Semantics.is_serial_solution_for_problem Ψ (rem_noops πs)"
by(induction πs)
(fastforce simp: SAS_Plus_Semantics.is_serial_solution_for_problem_def insert list.pred_set
prob_with_noop_def ListMem_iff rem_noops_def
sasp_filter_empty_action[unfolded empty_sasp_action_def rem_noops_def]
empty_sasp_action_def)+
lemma noops_valid: "is_valid_problem_sas_plus Ψ ⟹ is_valid_problem_sas_plus (prob_with_noop Ψ)"
by (auto simp: is_valid_problem_sas_plus_def prob_with_noop_def Let_def
empty_sasp_action_def is_valid_operator_sas_plus_def list.pred_set)
lemma sas_plus_problem_has_serial_solution_iff_i':
assumes "is_valid_problem_sas_plus Ψ"
and "𝒜 ⊨ Φ⇩∀ (φ (prob_with_noop Ψ)) t"
shows "SAS_Plus_Semantics.is_serial_solution_for_problem Ψ
(rem_noops
(map (λop. φ⇩O¯ (prob_with_noop Ψ) op)
(concat (Φ¯ (φ (prob_with_noop Ψ)) 𝒜 t))))"
using assms noops_valid
by(force intro!: noops_sound sas_plus_problem_has_serial_solution_iff_i)
lemma sas_plus_problem_has_serial_solution_iff_ii':
assumes "is_valid_problem_sas_plus Ψ"
and "SAS_Plus_Semantics.is_serial_solution_for_problem Ψ ψ"
and "length ψ ≤ h"
shows "∃𝒜. (𝒜 ⊨ Φ⇩∀ (φ (prob_with_noop Ψ)) h)"
using assms
by(fastforce
intro!: assms noops_valid noops_complete
sas_plus_problem_has_serial_solution_iff_ii
[where ψ = "(replicate (h - length ψ) empty_sasp_action) @ ψ"] )
end