A SAT-based solver for Q-ALL SAT

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. Categories and Subject Descriptors

• Type: Conference
• Year: 2006
• Where: ACMSE
• Authors: Ben Browning, Anja Remshagen
• Keywords: ACMSE 2006, Q-ALL SAT, Sat Solver, State-of-the-art Solvers, Theoretical Computer Science