---
title: "Complementary Branching for #SAT: Bounded-Degree Bounds and Faster #3-SAT"
authors:
  - "Konstantin Kutzkov"
doi: "10.24963/ijcai.2026/254"
url: "https://ijcai.org/proceedings/2026/254"
pdf: "https://ijcai.org/proceedings/2026/0254.pdf"
venue: "Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence"
year: 2026
pages: "2282-2290"
track: "Main Track"
keywords:
  - "Constraint Satisfaction and Optimization: Solvers and tools"
  - "Constraint Satisfaction and Optimization: Satisfiabilty"
---

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

Konstantin Kutzkov

*Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence*, pages 2282-2290. DOI: [10.24963/ijcai.2026/254](https://doi.org/10.24963/ijcai.2026/254)

## 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.