2018/03/20 by Bernd Schuh, Schuh, Bernd
Computer Science · #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Formal Methods in Verification
paper · pdf · doi:10.48550/arxiv.1803.07376
openalex publication_date 2018/03/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.