The Long, the Short and the Random

TL;DR

This paper presents evidence for a deterministic algorithm capable of exactly counting satisfying assignments in certain random sparse SAT instances within sub-exponential time, leveraging a combinatorial property of CNF formulas.

Contribution

It introduces a novel deterministic algorithm for counting solutions in random sparse SAT problems, based on a new combinatorial property of CNF formulas.

Findings

Existence of a deterministic sub-exponential time algorithm for certain SAT instances

The algorithm exploits a combinatorial relation between unsatisfying assignments and monotone sub-formulae

Empirical and theoretical evidence support the algorithm's effectiveness

Abstract

We furnish solid evidence, both theoretical and empirical, towards the existence of a deterministic algorithm for random sparse $\#\Omega(\log n)$-SAT instances, which computes the exact counting of satisfying assignments in sub-exponential time. The algorithm uses a nice combinatorial property that every CNF formula has, which relates its number of unsatisfying assignments to the space of its monotone sub-formulae.