Complementary Branching for #SAT: Bounded-Degree Bounds and Faster #3-SAT

Kutzkov, Konstantin

doi:10.24963/ijcai.2026/254

Complementary Branching for #SAT: Bounded-Degree Bounds and Faster #3-SAT

Konstantin Kutzkov

Download BibTeX Cite

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence. Main Track. Pages 2282-2290.

https://doi.org/10.24963/ijcai.2026/254

Keywords

Constraint Satisfaction and Optimization: Solvers and tools
Constraint Satisfaction and Optimization: Satisfiabilty

Abstract

We present complementary branching, a new branching approach for model counting based on the complement counting paradigm. Instead of branching on individual variables, complementary branching decomposes the counting problem for arbitrary CNF formulas into several subformulas, which naturally augments the classic DPLL branching. We show two novel results in which the main tool is complementary branching. First, we design new #SAT algorithms for sparse CNF formulas running in time O*(2^(alpha n)), for some constant alpha < 1. As a second application, we improve the best known deterministic upper bound for #3-SAT to O*(1.637^n) by using a version of clause learning based on complementary branching. These results demonstrate that complementary branching is a powerful tool for designing faster exact algorithms for propositional model counting.

Konstantin Kutzkov. 2026. Complementary Branching for #SAT: Bounded-Degree Bounds and Faster #3-SAT. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26. IJCAI, 2282–2290. https://doi.org/10.24963/ijcai.2026/254

@inproceedings{ijcai2026p254,
  title     = {Complementary Branching for #SAT: Bounded-Degree Bounds and Faster #3-SAT},
  author    = {Kutzkov, Konstantin},
  booktitle = {Proceedings of the Thirty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-26}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Diego Calvanese},
  pages     = {2282--2290},
  year      = {2026},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2026/254},
  url       = {https://doi.org/10.24963/ijcai.2026/254},
}

TY  - CPAPER
TI  - Complementary Branching for #SAT: Bounded-Degree Bounds and Faster #3-SAT
AU  - Kutzkov, Konstantin
T2  - Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2026
SP  - 2282
EP  - 2290
DO  - 10.24963/ijcai.2026/254
UR  - https://doi.org/10.24963/ijcai.2026/254
ER  -