ABT with Clause Learning for Distributed SAT

Abstract

Transforming a planning instance into a propositional formula ϕ 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 ϕ distributed among agents –each agent knows a part of ϕ but no agent knows the whole ϕ–, check if ϕ 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. © Springer International Publishing Switzerland 2016