A competitive and cooperative approach to propositional satisfiability

被引:12
|
作者
Inoue, Katsumi
Soh, Takehide
Ueda, Seiji
Sasaura, Yoshito
Banbara, Mutsunori
Tamura, Naoyuki
机构
[1] Natl Inst Informat, Chiyoda Ku, Tokyo 1018430, Japan
[2] Kobe Univ, Grad Sch Sci & Technol, Kobe, Hyogo 6578501, Japan
[3] Kobe Univ, Dept Elect & Elect Engn, Kobe, Hyogo 6578501, Japan
[4] Kobe Univ, Informat Sci & Technol Ctr, Kobe, Hyogo 6578501, Japan
关键词
SAT; SAT solver; parallel execution; planning; job-shop scheduling;
D O I
10.1016/j.dam.2006.04.015
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
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. (c) 2006 Elsevier B.V. All rights reserved.
引用
收藏
页码:2291 / 2306
页数:16
相关论文
共 50 条
  • [1] A simple approach to solving cooperative path-finding as propositional satisfiability works well
    Surynek, Pavel
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8862 : 827 - 833
  • [2] A Simple Approach to Solving Cooperative Path-Finding as Propositional Satisfiability Works Well
    Surynek, Pavel
    PRICAI 2014: TRENDS IN ARTIFICIAL INTELLIGENCE, 2014, 8862 : 827 - 833
  • [3] Mutex Reasoning in Cooperative Path Finding Modeled as Propositional Satisfiability
    Surynek, Pavel
    2013 IEEE/RSJ INTERNATIONAL CONFERENCE ON INTELLIGENT ROBOTS AND SYSTEMS (IROS), 2013, : 4326 - 4331
  • [4] A finite state intersection approach to propositional satisfiability
    Castano, Jose M.
    Castano, Rodrigo
    THEORETICAL COMPUTER SCIENCE, 2012, 450 : 92 - 108
  • [5] A propositional satisfiability approach in mining compact rules
    Bakar, AA
    Sulaiman, MN
    Othman, M
    Selamat, MH
    DATA MINING III, 2002, 6 : 197 - 204
  • [6] Variable and Clause Ordering in an FSA Approach to Propositional Satisfiability
    Castano, Jose M.
    Castano, Rodrigo
    IMPLEMENTATION AND APPLICATION OF AUTOMATA, 2011, 6807 : 76 - 87
  • [7] From propositional satisfiability to satisfiability modulo theories
    Sheini, Hossein M.
    Sakallah, Karem A.
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS, 2006, 4121 : 1 - 9
  • [8] SATISFIABILITY PROBLEMS FOR PROPOSITIONAL CALCULI
    LEWIS, HR
    MATHEMATICAL SYSTEMS THEORY, 1979, 13 (01): : 45 - 53
  • [9] Symbolic Techniques in Propositional Satisfiability Solving
    Vardi, Moshe Y.
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2009, PROCEEDINGS, 2009, 5584 : 2 - 3
  • [10] Economic sanctions as the propositional satisfiability problem
    Dragan Miljkovic
    Policy Sciences, 2002, 35 : 1 - 15