NEW WORST-CASE UPPER BOUND FOR COUNTING EXACT SATISFIABILITY

作者:Zhou, Junping*; Su, Weihua; Wang, Jianan
来源:International Journal of Foundations of Computer Science, 2014, 25(6): 667-678.
DOI:10.1142/S0129054114500270

摘要

The counting exact satisfiablity problem (#XSAT) is a problem that computes the number of truth assignments satisfying only one literal in each clause. This paper presents an algorithm that solves the #XSAT problem in O(1.1995(n)), which is faster than the best algorithm running in O(1.2190(n)), where n denotes the number of variables. To increase the efficiency of the algorithm, a new principle, called common literals principle, is addressed to simplify formulae. This allows us to further eliminate literals. In addition, we firstly apply the resolution principles into solving #XSAT problem, and therefore it improves the efficiency of the algorithm further.