ABT with Clause Learning for Distributed SAT.

Transforming a planning instance into a propositional formula phi to be solved by a SAT solver is a common approach in AI planning. In the context of multiagent planning, this approach causes the distributed SAT problem: given phi distributed among agents -each agent knows a part of phi but no agent knows the whole phi-, check if phi is SAT or UNSAT by message passing. On the other hand, Asynchronous Backtracking (ABT) is a complete distributed constraint satisfaction algorithm, so it can be directly used to solve distributed SAT. Clause learning is a technique, commonly used in centralized SAT solvers, that can be applied to enhance ABT efficiency when used for distributed SAT. We prove that ABT with clause learning remains correct and complete. Experiments on several planning benchmarks show very substantial benefits for ABT with clause learning.