A competitive and cooperative approach to propositional satisfiability

Propositional satisfiability (SAT) has attracted considerable attention recently in both Computer Science and Artificial Intelligence, and a lot of algorithms have been developed for solving SAT. Each SAT solver has strength and weakness, and it is difficult to develop a universal SAT solver which can efficiently solve a wide range of SAT instances. We thus propose parallel execution of SAT solvers each of which individually solves the same SAT instance simultaneously. With this competitive approach, a variety of SAT instances can be solved efficiently in average. We then consider a cooperative method for solving SAT by exchanging lemmas derived by conflict analysis among different SAT solvers. To show the usefulness of our approach, we solve SATLIB benchmark problems, planning benchmark problems as well as the job-shop scheduling problem with good performance. The system has been implemented in Java with both systematic and stochastic solvers.