A Solver for Quantied Formula Problem Q-ALL SAT
Anja Remshagen, Klaus Truemper · 2008
Problem Q-ALL SAT demands solving a quantied Boolean formula that involves two propositional formulas in conjunctive normal form (CNF). When the rst formula has no clauses and thus is trivial, Q-ALL SAT becomes the standard quantied Boolean formula (QBF) at the second level of the polynomial hierarchy. In general, Q-ALL SAT can be converted to second-level QBF by well-known transformations. A number of application problems can be formulated as instances of Q-ALL SAT. Thus, solution of the problem is of practical importance. This paper describes a solution algorithm for Q-ALL SAT called QRSsat3. The method is a signicant improvement over an algorithm called QRSsat that was described in an earlier paper. Algorithm QRSsat3 relies on backtracking search just as QRSsat does. The improvement over the predecessor is due to an enhanced learning process and a heuristic for the satisability problem SAT of CNF formulas. Computational results are reported for three sets of instances including a robot problem and a game problem. To compare the performance of QRSsat3 with other solvers, we have converted the test instances into QBF format required by QBF solvers. For these test instances, QRSsat3 has uniformly low solution times and is substantially faster than QRSsat, which in turn was already much faster than state-of-the-art QBF solvers. The problems SAT and Q-ALL SAT are part of a previously dened hierarchy of quantied formulas that we call constrained quantied formulas (CQFs). The paper includes some complexity results for the hierarchy of specially structured CQFs and thus for specially structured Q-ALL SAT cases.