The Exact Satisfiability problem, XSAT, is defined as the problem of finding a satisfying assignment to a formula $\varphi$ in CNF such that exactly one literal in each clause is assigned to be "1" and the other literals in the same clause are set to "0". Since it is an important variant of the satisfiability problem, XSAT has also been studied heavily and has seen numerous improvements to the development of its exact algorithms over the years. The fastest known exact algorithm to solve XSAT runs in $O(1.1730^n)$ time, where $n$ is the number of variables in the formula. In this paper, we propose a faster exact algorithm that solves the problem in $O(1.1674^n)$ time. Like many of the authors working on this problem, we give a DPLL algorithm to solve it. The novelty of this paper lies on the design of the nonstandard measure, to help us to tighten the analysis of the algorithm further.
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。