New Worst-Case Upper Bounds for X2SAT

The problem of X2SAT is a generalized problem of XSAT. Given a conjunctive normal function, this problem asks whether there exists a satisfying assignment for the input formula, such that exactly two literals in each clause are true. The rigorous theoretical analysis of the algorithms for solving X2SAT problem is proposed in the literature. An algorithm X2SAT-N based on Davis-Putnam-Logemann-Loveland (DPLL) is first presented to solve the X2SAT problem. In the algorithm X2SAT-N, a simplification process is first called to simplify the input formula. After that, several strategies are used to cut the branches on different kinds of clauses. It can be proved that the worst-case upper bound of algorithm X2SAT-N for solving X2SAT should be O(1.4203n), which improves the previous fastest X2SAT algorithm of O(1.4511n) up to now. Here n denotes the number of variables in a formula. Additionally, an algorithm called as X2SAT-L for solving X2SAT problem is also presented. This algorithm is also based on DPLL and using similar simplification process. We prove that the worst-case upper bound of this algorithm is O(1.3643l), where l is the length of the formula. Within our knowledge, this algorithm is the best algorithm for X2SAT with the parameter of the length of the formula.