SARRIGUREN: a polynomial-time complete algorithm for random $k$-SAT with relatively dense clauses

TL;DR

SARRIGUREN introduces a complete SAT algorithm based on counting unsatisfying variations via full-clause expansions and inclusion–exclusion. It achieves polynomial-time behavior on random dense $k$-SAT instances (notably when $k \,\ge\,7\sqrt{n}$), due to vanishing clause overlaps, and extends to #SAT and Unique-SAT. The method relies on constructs like $K^{full}$ and $\overline{K}^{full}$, with complexity governed by $O\bigl(m^{2}\times \tfrac{n}{k}\bigr)$ in the dense regime, supported by empirical results and complementary solvers that recover solutions and per-literal counts. While not resolving NP=P for 3-SAT, the work broadens the landscape by showing sub-exponential-like behavior for dense random instances and suggests practical heuristics and parallelizations for future SAT-solvers work.

Abstract

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.

Figures (2)

• Figure 1: Graphics for each M showing times depending on N and density types
• Figure 2: Graphics for each density type showing times depending on N and M