Jesús Giráldez-Cru, Pedro Meseguer

ABT with Clause Learning for Distributed SAT

CAEPIA 2016

Transforming a planning instance into a propositional formula Φ to be solved by a SAT solver is a common approach in classical 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. Experimentally, we show very substantial benefits for ABT with clause learning, on several planning benchmarks.