Algorithms Based On DPLL For The NAE-3SAT And The#NAE-3SAT

The Satisfiability problem (SAT) and the Model Counting problem (#SAT) aretwo important issues in the field of automated reasoning. They have been widely usedin the areas of intelligent planning, machine vision, probabilistic inference, logictheory machine and so on.The Not-All-Equal Satisfiability problem (NAESAT) and the#Not-All-EqualSatisfiability problem (#NAESAT) are important extension of the SAT problem andthe#SAT problem. The NAESAT problem is NP-complete and the#NAESATproblem is#P-complete. The NAESAT problem asks whether the given CNF formulaF is NAE-satisfiable, which means that there is a truth assignment of the formula Fnot only makes the formula F satisfiable and also makes the values for all the literalsin each clause of the formula F not all equal (at least one literal is assigned true andone literal is assigned false). The#NAESAT problem is to compute the number ofNAE-satisfiability assignments for the given CNF formula. The NAESAT problemand the#NAESAT problem are widely used in the areas of the Maxcut problem, theDomatic Number problem, the Probabilistic Inference problem and so on.In the paper, two complete algorithms NAE and CNAE based on the Davis-P-utnam-Logemann-Loveland (DPLL) for the NAE-3SAT problem and the#NAE3SATproblem are proposed. In the two algorithms, a variety of new reduction rules are usedto simplify the formulas. The reduction rules play an important role on improving theefficiency of the algorithms. By analyzing, we prove that the two algorithms NAE andCNAE for the NAE-3SAT problem and the#NAE-3SAT problem are complete andthe worst-case upper bounds for both the two algorithms are O(1.618n), where n is thenumber of variables in the formula, which are both best upper bounds up to nowwithin our knowledge.