Distributed SAT

摘要

We present DPLL ABT, a distributed Satisfiability solver (SAT) (Ansótegui and Manyà in IberoAm J Artif Intell 7(20):43–56, 2003) designed to solve distributed SAT problem instances. Since SAT is a particular case of constraint satisfaction, we propose a solving method based on the Asynchronous Backtracking algorithm (ABT) (Yokoo et al. in IEEE Trans Knowl Data Eng 10(5):673–685, 1998) developed for distributed constraint reasoning. In addition, we have applied the Davis-Putnam procedure (DPLL) in every agent, plus the minimum conflict heuristic in case DPLL does not detect any inconsistency. The resulting algorithm improves the performance in terms of communication cost and computational effort versus the basic ABT. The SAT instance is distributed into agents, which cooperate to solve SAT instances just sharing the minimum information. We also present the experimental results that demonstrate the performance of the method in terms of communication and execution time comparing the performance with the basic ABT algorithm.