New Algorithms for #2-SAT and #3-SAT

TL;DR

This paper presents significantly faster algorithms for weighted #2-SAT and #3-SAT problems, improving upon previous methods through novel reduction rules and advanced analysis techniques.

Contribution

It introduces new algorithms with improved exponential time bounds for weighted #2-SAT and #3-SAT, utilizing innovative reduction rules and graph decomposition methods.

Findings

Weighted #2-SAT solved in O*(1.1082^m) time

Weighted #3-SAT solved in O*(1.4423^m) time

Significant improvements over previous algorithms

Abstract

The #2-SAT and #3-SAT problems involve counting the number of satisfying assignments (also called models) for instances of 2-SAT and 3-SAT, respectively. In 2010, Zhou et al. proposed an $\mathcal{O}^*(1.1892^m)$-time algorithm for #2-SAT and an efficient approach for #3-SAT, where $m$ denotes the number of clauses. In this paper, we show that the weighted versions of #2-SAT and #3-SAT can be solved in $\mathcal{O}^*(1.1082^m)$ and $\mathcal{O}^*(1.4423^m)$ time, respectively. These results directly apply to the unweighted cases and achieve substantial improvements over the previous results. These advancements are enabled by the introduction of novel reduction rules, a refined analysis of branching operations, and the application of path decompositions on the primal and dual graphs of the formula.