Theory SAT_Solve_SAS_Plus

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
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 ψ" 
  (* TODO refactor *)
  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 termt 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