SMT-Based Reasoning and Planning in TAL
Magnus Hällin · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2010
Automated planning as a satisfiability problem is a method developed in theearly nineties. It has some known disadvantages, such as its inefficient encod-ing of numbers. The field of Satisfiability Modulo Teories tries to connectalready established solvers for e.g. linear constraints into SAT-solvers in orderto make reasoning about numerical values more efficient. This thesis combines planning as satisfiability and SMT to perform efficientreasoning about actions that occupy realistic time in Temporal Action Logic,a formalism developed at Linköping University for reasoning about action andchange.