New Worst-Case Upper Bound for #XSAT

TL;DR

This paper introduces a faster algorithm for #XSAT model counting with a new principle and resolution techniques, significantly improving the worst-case upper bound over previous methods.

Contribution

It presents the first application of resolution principles and a novel common literals principle to enhance #XSAT counting efficiency, achieving a new worst-case upper bound.

Findings

New algorithm runs in O(1.1995^n) time

Improves upon previous O(1.2190^n) bound

Introduces common literals and resolution principles

Abstract

An algorithm running in O(1.1995n) is presented for counting models for exact satisfiability formulae(#XSAT). This is faster than the previously best algorithm which runs in O(1.2190n). In order to improve the efficiency of the algorithm, a new principle, i.e. the common literals principle, is addressed to simplify formulae. This allows us to eliminate more common literals. In addition, we firstly inject the resolution principles into solving #XSAT problem, and therefore this further improves the efficiency of the algorithm.