Project Abstract:

The planning problem is one of the challenging problems in artificial intelligence. There exist many efforts to efficiently solve the planning problem. One promising approach to planning is based on the use of SAT solvers. However, most of the existing SAT-based planners are doing the solution extraction in a non-deterministic way, using the backtracking strategy. Our paper describes a new alternative by proposing a deterministic approach for solving the planning problem using counting satisfiability. We provide a better alternative for guiding planning and search, where the number of truth assignments would help lead to a goal. For efficiency reasons, our technique is applied incrementally, so that only the new added sub-formulas are computed by avoiding the re-computation of the whole problem. Experimental results show that our counting SAT solver is comparable to the state-of-the-art SAT solvers that have been adopted by the existing planners.

Project Abstract:

Looking for subclasses of formulas for which the SAT problem can be solved in polynomial time is one of important challenges in computer science. We present a new subclass of formulas for which the SAT and counting SAT problem can be solved in polynomial time. Specifically, our novel algorithm operates on conjunctive normal form propositional formula in which all pairs of clauses are coupled, i.e., there exists at least one literal in one clause that appears negated in the other. This subclass of formulas is different than previously known subclasses that are solvable in polynomial time. This is an improvement over the SAT Dichotomy Theorem [Sch78] and the counting SAT Dichotomy Theorem [CrH96], since our subclass can be moved out from the NP-complete class to P. The membership problem for this new subclass can be done in O(n* l^2), where n and l are the number of variables and clauses, respectively. Moreover, the algorithm can also be used to approximate the counting SAT problem for arbitrary conjunctive normal form propositional formulas in that it generates an upper bound for the number of assignments that satisfy the formula.