SARRIGUREN, a new complete algorithm for SAT based on counting clauses (which is valid also for Unique-SAT and #SAT) is described, analyzed and tested. Although existing complete algorithms for SAT perform slower with clauses with many literals, that is an advantage for SARRIGUREN, because the more literals are in the clauses the bigger is the probability of overlapping among clauses, a property that makes the clause counting process more efficient. Actually, it provides a $O(m^2 \times n/k)$ time complexity for random $k$-SAT instances of $n$ variables and $m$ relatively dense clauses, where that density level is relative to the number of variables $n$, that is, clauses are relatively dense when $k\geq7\sqrt{n}$. Although theoretically there could be worst-cases with exponential complexity, the probability of those cases to happen in random $k$-SAT with relatively dense clauses is practically zero. The algorithm has been empirically tested and that polynomial time complexity maintains also for $k$-SAT instances with less dense clauses ($k\geq5\sqrt{n}$). That density could, for example, be of only 0.049 working with $n=20000$ variables and $k=989$ literals. In addition, they are presented two more complementary algorithms that provide the solutions to $k$-SAT instances and valuable information about number of solutions for each literal. Although this algorithm does not solve the NP=P problem (it is not a polynomial algorithm for 3-SAT), it broads the knowledge about that subject, because $k$-SAT with $k>3$ and dense clauses is not harder than 3-SAT. Moreover, the Python implementation of the algorithms, and all the input datasets and obtained results in the experiments are made available.

翻译：本文描述、分析并测试了SARRIGUREN——一种基于子句计数的SAT新完备算法（同时适用于Unique-SAT和#SAT）。尽管现有SAT完备算法在处理含多文字子句时表现较慢，但这反而成为SARRIGUREN的优势：子句中文字越多，子句间重叠概率越大，而该特性可使子句计数过程效率更高。具体而言，对于包含$n$个变量和$m$个相对稠密子句的随机$k$-SAT实例，该算法的时间复杂度为$O(m^2 \times n/k)$，其中稠密程度相对于变量数$n$定义，即当$k\geq7\sqrt{n}$时子句被视为相对稠密。尽管理论上可能存在指数复杂度的最坏情况，但此类情况在含相对稠密子句的随机$k$-SAT中发生概率几乎为零。实验测试表明，该多项式时间复杂度同样适用于稀疏子句的$k$-SAT实例（$k\geq5\sqrt{n}$）。例如，当$n=20000$个变量且$k=989$个文字时，该稠密度可低至0.049。此外，本文还提出两种互补算法，可提供$k$-SAT实例的解及其各文字解数量的重要信息。尽管该算法未能解决NP=P问题（并非针对3-SAT的多项式算法），但由于$k>3$且含稠密子句的$k$-SAT并不比3-SAT更难，因此拓宽了该领域认知。本文同时公开了算法的Python实现、所有输入数据集及实验所得结果。