B. Browning
ABSTRACT
Although the satisfiability problem (SAT) is NP-complete, state-of-the-art solvers for SAT can solve instances that are considered to be very hard. Emerging applications demand to solve even more complex problems residing at the second or higher levels of the polynomial hierarchy. We identify such a problem, called Q-ALL SAT, that arises in a variety of applications. We have designed a solution algorithm for Q-ALL SAT that employs a SAT solver and thus exploits the recent advances of SAT solvers. In addition, a heuristic is applied to reduce the number of instances that are to be solved by the SAT solver. A learning scheme improves the performance of that heuristic. Test results of a first implementation of the proposed algorithm confirm that this is a very promising approach.
- M. Cadoli, M. Schaerf, A. Giovanardi, and M. Giovanardi. An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation. Journal of Automated Reasoning, 28(2):101--142, 2002.]] Google Scholar
Digital Library
- T. Eiter and G. Gottlob. The Complexity of Logic-based Abduction. Journal of the Association for Computing Machinery 42:3--42, 1995.]] Google ScholarDigital Library
- E. Giunchiglia, M. Narizzano, and A. Tacchella. Learning for Quantified Boolean Logic Satisfiability. In Proceedings of the 18th National Conference on Artificial Intelligence, 2002.]] Google ScholarDigital Library
- E. Giunchiglia, M. Narrizano, and A. Tacchella. Backjumping for quantified boolean logic satisfiability. Artificial Intelligence, 145(1):99--120, 2003.]] Google ScholarDigital Library
- M. Mneimneh and K. Sakallah. Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing, 2003.]]Google Scholar
- C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.]]Google Scholar
- D. Ranjan, D. Tang, and S. Malik. A comparative study of 2qbf algorithms. In Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), 2004.]]Google Scholar
- A. Remshagen and K. Truemper. An Effective Algorithm for the Futile Questioning Problem. Journal of Automated Reasoning, 34(1):31--47, 2005]] Google ScholarDigital Library
- J. Rintanen. Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research, 10:323--352, 1999.]]Google ScholarDigital Library
- J. Rintanen. Partial implicit unfolding in the davis-putnam procedure for quantified boolean formula. In International Conference on Logic Programming, Artificial Intelligence and Reasoning, pages 362--376, 2001.]] Google ScholarDigital Library
- SAT 2005. Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing. Fahiem Bacchus and Toby Walsh (Eds.), Springer Verlag, Lecture Notes in Computer Science 3569, 2005.]]Google Scholar
- SAT Competitions. http://www.satcompetition.org. Daniel Le Berre and Laurent Simon (Organizing committee). 2002--2005.]]Google Scholar
- K. Truemper. Design of Logic-based Intelligent Systems. Wiley, 2004.]] Google ScholarDigital Library
- H. Zhang. SATO: an Efficient Propositional Prover. In Proceedings of the International Conference on Automated Deduction (CADE-97), pages 272--275, 1997.]] Google ScholarDigital Library
- L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In Proceedings of the International Conference on Computer Aided Design, 2001.]] Google ScholarDigital Library
- L. Zhang and S. Malik. Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation. In Proceedings of 8th International Conference on Principles and Practice of Constraint Programming, 2002.]] Google ScholarDigital Library
- L. Zhang and S. Malik. Conflict driven learning in a quantified boolean satisfiability solver. In Proceedings of the International Conference on Computer Aided Design, 2002.]] Google ScholarDigital Library
Index Terms
- A SAT-based solver for Q-ALL SAT
Recommendations
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)
We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason ...
A modular CNF-based SAT solver
SBCCI '10: Proceedings of the 23rd symposium on Integrated circuits and system designThe state-of-the-art SAT solvers, such as Chaff [11], zChaff [18], BerkMin [5], and Minisat [2] usually share the same core techniques, for instance: the watched literals structures conflict clause recording and non-chronological backtracking. ...
SAT Based BDD Solver for Quantified Boolean Formulas
ICTAI '04: Proceedings of the 16th IEEE International Conference on Tools with Artificial IntelligenceSolving Quantified Boolean Formulas (QBF) has become an attractive research area in Artificial intelligence. Many important artificial intelligence problems (planning, non monotonic reasoning, formal verification, etc.) can be reduced to QBFs. In this ...
Comments