Research On The Algorithm For The Subclass Of#SAT Based On DPLL

Intelligent planning is a cutting-edge research in the field of artificial intelligence.In recent years, this research has made revolutionary progress. Researchers haveproposed many methods to solve the planning problem, where a very efficient methodis that transform planning problems into propositional satisfiability (SAT) problems.However, there are many classical planning problems which can not be converted intothe SAT problem to solve. Some problems need to calculate the number of satisfyingassignments of the propositional formulas, which can be called model countingproblem, namely#SAT problem. In practical applications, in order to solve someproblems more easily, the researchers usually try to make the object propositionalformula’s logical structure as simple as possible. Model counting problems with thepropositional formula’s limited logical structure is referred to as the subclasses of#SAT problems. Therefore, promoting the subclass of#SAT problems have farpotential value for intelligent planning and even the artificial intelligence fields.In the various algorithms of solving SAT,#SAT and its sub-classes’ problems, theDPLL algorithm’s performance is the most efficient. But the time complexity of thealgorithm is also in the level of exponent. So, many researchers improve the DPLLalgorithm by presented new rules to simple propositional formula, or chose branchesfurther. At the same time, this idea has also spawned the discussion on the algorithms’upper bound of the time complexity at the worst case.In this paper, we choose#2-SAT problem as our research topic, and propose anew algorithm based on DPLL, we call it as PMC algorithm. As most of researchersuse the number of variables in propositional formula as parameter to analyze theupper bound of time complexity at the worst case, we start from the perspective of thenumber of clauses, use branch tree theory to analyze PMC algorithm, and prove that itimproves#2-SAT algorithm’s upper bound from O(1.1892m) to O(1.1740m). Moreover,we design the#2-SAT solver, and compare with the original#2-SAT algorithm. Theexperimental result show that PMC algorithm’s running time is significantly less thanthat of the original#2-SAT algorithm.