[HTML][HTML] A competitive and cooperative approach to propositional satisfiability

K Inoue, T Soh, S Ueda, Y Sasaura, M Banbara… - Discrete Applied …, 2006 - Elsevier
K Inoue, T Soh, S Ueda, Y Sasaura, M Banbara, N Tamura
Discrete Applied Mathematics, 2006Elsevier
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 …
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.
Elsevier
以上显示的是最相近的搜索结果。 查看全部搜索结果