  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.
