Jesús Giráldez-Cru, Guillermo Martín-Sánchez, Pedro Meseguer

Connecting ABT with a SAT Solver


Many real-world problems are nowadays encoded into SAT instances and efficiently solved by CDCL SAT solvers. However, some scenarios require distributed problem solving approaches. Privacy is often the main reason. This causes the distributed SAT problem. In this work, we analyze how this problem can be tacked in an efficient way, and present ABTSAT, a new version of the ABT algorithm adapted to solve distributed SAT instances. It combines ABT execution with calls to CDCL SAT solvers and clause learning. ABTSAT is sound and complete, properties inherited from ABT, and solves local problems efficiently by using CDCL SAT solvers.