Planningwith SAT Introduction Encodings SolverCalls Solving AI Planning Problems with SAT SATsolving Invariants Conclusion References JussiRintanen EPCL,Dresden,November2013 Reduction of AI Planning to SAT KautzandSelman1992[KS92] Planningwith SAT Introduction SolvingtheAIplanningproblemwithSATalgorithms Earlyworks Significance Novelty: planningearlierviewedasadeductionproblem Formalizations Encodings Idea: SolverCalls propositionalvariablesforeverystatevariableforeverytime SATsolving point Invariants clausesthatdescribehowstatecanchangebetweentwo Conclusion consecutivetimepoints References unitclausesspecifyingtheinitialstateandgoalstates TestmaterialforlocalsearchalgorithmGSAT[SLM92] ResultingSATproblemsthatcouldbesolvedhadupto1000 variablesand15000clauses. Reduction of AI Planning to SAT KautzandSelman1992[KS92] Planningwith SAT Introduction SolvingtheAIplanningproblemwithSATalgorithms Earlyworks Significance Novelty: planningearlierviewedasadeductionproblem Formalizations Encodings Idea: SolverCalls propositionalvariablesforeverystatevariableforeverytime SATsolving point Invariants clausesthatdescribehowstatecanchangebetweentwo Conclusion consecutivetimepoints References unitclausesspecifyingtheinitialstateandgoalstates TestmaterialforlocalsearchalgorithmGSAT[SLM92] ResultingSATproblemsthatcouldbesolvedhadupto1000 variablesand15000clauses. Reduction of AI Planning to SAT KautzandSelman1992[KS92] Planningwith SAT Introduction SolvingtheAIplanningproblemwithSATalgorithms Earlyworks Significance Novelty: planningearlierviewedasadeductionproblem Formalizations Encodings Idea: SolverCalls propositionalvariablesforeverystatevariableforeverytime SATsolving point Invariants clausesthatdescribehowstatecanchangebetweentwo Conclusion consecutivetimepoints References unitclausesspecifyingtheinitialstateandgoalstates TestmaterialforlocalsearchalgorithmGSAT[SLM92] ResultingSATproblemsthatcouldbesolvedhadupto1000 variablesand15000clauses. Reduction of AI Planning to SAT KautzandSelman1992[KS92] Planningwith SAT Introduction SolvingtheAIplanningproblemwithSATalgorithms Earlyworks Significance Novelty: planningearlierviewedasadeductionproblem Formalizations Encodings Idea: SolverCalls propositionalvariablesforeverystatevariableforeverytime SATsolving point Invariants clausesthatdescribehowstatecanchangebetweentwo Conclusion consecutivetimepoints References unitclausesspecifyingtheinitialstateandgoalstates TestmaterialforlocalsearchalgorithmGSAT[SLM92] ResultingSATproblemsthatcouldbesolvedhadupto1000 variablesand15000clauses. Significance Planningwith SAT Planningoneofthefirst“real”applicationsforSAT(others: Introduction Earlyworks graph-coloring,testpatterngeneration,...) Significance Formalizations Later,sameideasappliedtootherreachabilityproblems: Encodings computer-aidedverification(BoundedModel-Checking SolverCalls [BCCZ99]) SATsolving DESdiagnosabilitytesting[RG07]anddiagnosis[GARK07] Invariants SATandrelatedmethodscurrentlyaleadingapproachto Conclusion References solvingstatespacereachabilityproblemsinAIandother areasofCS. Overlookedconnection: theencodingisveryclosetoCook’s reductionfromP-timeTuringmachinestoSATinhisproofof NP-hardnessofSAT[Coo71]. Significance Planningwith SAT Planningoneofthefirst“real”applicationsforSAT(others: Introduction Earlyworks graph-coloring,testpatterngeneration,...) Significance Formalizations Later,sameideasappliedtootherreachabilityproblems: Encodings computer-aidedverification(BoundedModel-Checking SolverCalls [BCCZ99]) SATsolving DESdiagnosabilitytesting[RG07]anddiagnosis[GARK07] Invariants SATandrelatedmethodscurrentlyaleadingapproachto Conclusion References solvingstatespacereachabilityproblemsinAIandother areasofCS. Overlookedconnection: theencodingisveryclosetoCook’s reductionfromP-timeTuringmachinestoSATinhisproofof NP-hardnessofSAT[Coo71]. Classical (Deterministic, Sequential) Planning ∼succincts-t-reachabilityproblemforgraphs Planningwith SAT Introduction Earlyworks Significance statesandactionsexpressedintermsofstatevariables Formalizations singleinitialstate,thatisknown Encodings SolverCalls allactionsdeterministic SATsolving actionstakensequentially,oneatatime Invariants Conclusion agoalstate(expressedasaformula)reachedintheend References DecidingwhetheraplanexistsisPSPACE-complete. Withapolynomialboundonplanlength,NP-complete. Formalization Planningwith SAT Introduction Earlyworks Aprobleminstancein(classical)planningconsistsofthe Significance Formalizations following. Encodings setX ofstatevariables SolverCalls SATsolving setAofactions(cid:104)p,e(cid:105)where Invariants pistheprecondition(asetofliteralsoverX) Conclusion eistheeffects(asetofliteralsoverX) References initialstateI :X →{0,1}(avaluationofX) goalsG(asetofliteralsoverX) The planning problem Planningwith SAT Introduction Earlyworks Anactiona=(cid:104)p,e(cid:105)isapplicableinstatesiffs|=p. Significance Formalizations Thesuccessorstates(cid:48) =exec (s)isdefinedby a Encodings s(cid:48) |=e SolverCalls s(x)=s(cid:48)(x)forallx∈X thatdon’toccurine. SATsolving Invariants Conclusion Problem References Finda ,...,a suchthat 1 n exec (exec (···exec (exec (I))···))|=G? an an−1 a2 a1