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

2025/07/19 by Peng, Junqiang, Sheng, Zimo, Xiao, Mingyu
#Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences

paper · doi:10.48550/arxiv.2507.14504

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 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 O^*(1.1082^m) and 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.

Citations

• Solving Projected Model Counting by Utilizing Treewidth and its Limits
• DPMC: Weighted Model Counting by Dynamic Programming on Project-Join\n Trees
• New worst upper bound for #SAT
• A universally fastest algorithm for Max 2-Sat, Max 2-CSP, and everything in between
• On probabilistic inference by weighted model counting

Related

• New worst upper bound for #SAT
• A Faster Exact Algorithm to Count X3SAT Solutions
• A Polynomial Time Algorithm for 3-SAT
• Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT
• An exact algorithm for 1-in-3 SAT