论文标题
更快的精确算法来计算X3SAT解决方案
A Faster Exact Algorithm to Count X3SAT Solutions
论文作者
论文摘要
确切的令人满意的问题XSAT被定义为在CNF中找到令人满意的分配的问题，以使每个条款中完全存在一个字面意义，而同一条款中的其他文字则将其设置为0。如果我们将每个条款的长度限制为大多数3个文字，则已知为X3SAT问题。在本文中，我们考虑了计算X3SAT问题满足分配数量的问题，这也称为＃x3SAT。 当前最先进的算法要解决＃x3SAT，由Dahllöf，Jonsson和Beigel提供，并以$ O（1.1487^n）$运行，其中$ n $是公式中的变量数量。在本文中，我们提出了一种以$ O（1.1120^n）$运行的＃x3SAT问题的精确算法，而很少有分支案例可以考虑使用Monien和Preis的结果，以给我们提供最多图3的图形的二分线宽度。
The Exact Satisfiability problem, XSAT, is defined as the problem of finding a satisfying assignment to a formula in CNF such that there is exactly one literal in each clause assigned to be 1 and the other literals in the same clause are set to 0. If we restrict the length of each clause to be at most 3 literals, then it is known as the X3SAT problem. In this paper, we consider the problem of counting the number of satisfying assignments to the X3SAT problem, which is also known as #X3SAT. The current state of the art exact algorithm to solve #X3SAT is given by Dahllöf, Jonsson and Beigel and runs in $O(1.1487^n)$, where $n$ is the number of variables in the formula. In this paper, we propose an exact algorithm for the #X3SAT problem that runs in $O(1.1120^n)$ with very few branching cases to consider, by using a result from Monien and Preis to give us a bisection width for graphs with at most degree 3.
