Sub-exponential Upper Bound for #XSAT of some CNF Classes

TL;DR

This paper presents a new sub-exponential upper bound on the number of solutions for certain CNF formulas in XSAT, based on literal distribution, with implications for broader SAT problem classes.

Contribution

It introduces a novel sub-exponential bound for XSAT models that depends solely on literal distribution, extending to broader SAT classes.

Findings

Derived a sub-exponential upper bound for XSAT models

Bound computable in O(exp(sqrt(n))) time for specific CNF subsets

Extended method applicability to wider SAT problem classes

Abstract

We derive an upper bound on the number of models for exact satisfiability (XSAT) of arbitrary CNF formulas F. The bound can be calculated solely from the distribution of positive and negated literals in the formula. For certain subsets of CNF instances the new bound can be computed in sub-exponential time, namely in at most O(exp(sqrt(n))) , where n is the number of variables of F. A wider class of SAT problems beyond XSAT is defined to which the method can be extended.