Implementing an action language using a SAT solver

In recent years, research on planning algorithms has made big progress. Recent approaches encode the plan search space into a data structure called the planning graph. To extract plans, a planning graph is transformed into the satisfiability problem (SAT), which is solved by a high-speed SAT solver. This kind of planning is called SAT planning. On the other hand, recent research on reasoning about action has also progressed. Since Gelfond and Lifschitz (1993) proposed the action language 𝒜, a lot of work has been done to improve action languages. We combine these two approaches. Namely, we extend techniques for SAT planning to cover other aspects of reasoning about action, so that various types of queries can be answered for action languages. For this purpose, we implemented an action language processing system AMP in Java. Using this system, it becomes possible to answer queries for not only planning but model generation for a domain description written in the action language 𝒜