论文标题
改进的确切算法，以解决确切的可满足性问题
An Improved Exact Algorithm for the Exact Satisfiability Problem
论文作者
论文摘要
确切的满足性问题XSAT被定义为在CNF中找到满足的分配的问题，以使每个子句中的一个字面恰好分配为“ 1”，而同一条款中的其他文字则将其设置为“ 0”。由于它是令人满意问题的重要变体，因此XSAT也经过了大量研究，并且多年来对其确切算法的开发进行了许多改进。 求解XSAT的最快已知算法以$ O（1.1730^n）$时间运行，其中$ n $是公式中的变量数量。在本文中，我们提出了一种更快的精确算法，以$ O（1.1674^n）$时间解决该问题。像许多研究此问题的作者一样，我们给出了DPLL算法来解决它。本文的新颖性在于非标准度量的设计，以帮助我们进一步收紧算法的分析。
The Exact Satisfiability problem, XSAT, is defined as the problem of finding a satisfying assignment to a formula $φ$ 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.
