Research map / Probabilistic and scientific modeling / Variational and generative sampling
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes Koco-SMC, an exact Satisfiability Modulo Counting solver that embeds probabilistic-circuit-based upper/lower bound tracking (Upper-Lower Watch) into a MiniSAT CDCL loop for early conflict detection.
Problem
Exactly solving Satisfiability Modulo Counting (SMC) problems, which combine Boolean SAT constraints with probabilistic marginal-inference thresholds (NP^PP-complete); existing exact approaches alternate between SAT and inference solvers with heavy back-and-forth overhead and slow unsat detection.
Approach
Compile each probabilistic factor into a smooth, decomposable probabilistic circuit and propagate upper and lower bounds on the marginal probability bottom-up as variables are assigned (Upper-Lower Watch), so conflicts with probabilistic constraints are detected on partial assignments and turned into learned clauses inside a CDCL loop.
Key results
- Koco-SMC solves 45% of SMC instances within 10 seconds, whereas exact baselines need up to 3 hours for a similar rate.
- Given a 3-hour limit, Koco-SMC solves 85% of instances.
- ULW propagation speeds Koco-SMC by about 10x over the variant without ULW on hard thresholds.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use Koco-SMC instead of exact SAT-plus-inference baselines | SMC benchmark dataset · SMC benchmark dataset | instances solved within 10 seconds: 45% | Helped |
| use Koco-SMC instead of exact solver baselines | SMC benchmark dataset · SMC benchmark dataset | instances solved within 3 hours: 85% vs. at most 40% | Helped |
| add ULW propagation (ablation) | Koco-SMC · SMC instance with threshold 10^6 | runtime speedup: 10 times | Helped |
| add ULW propagation (ablation) | Koco-SMC · SMC problems solvable in around 10 minutes | runtime speedup: 10 times | Helped |
| use Koco-SMC rather than approximate solvers | SMC benchmark dataset · SMC benchmark dataset | solution correctness | Helped |
| use Koco-SMC rather than exact SAT-plus-inference solvers | SMC benchmark dataset · SMC benchmark dataset | runtime | Helped |
Limitations
- Experiments fix the number of probabilistic constraints to one
- Compilation overhead makes Koco-SMC slower at low thresholds
- Hardest medium-threshold instances still time out for the exact solver
Experimental setup
Datasets: UAI Competition partition function benchmarks (50 instances) CNFgen 3-coloring grid instances
Benchmarks: 1,350 SMC problems built from UAI partition function instances and CNFgen 3-coloring formulas robust supply chain design networks package delivery Los Angeles graphs
Metrics: fraction of instances solved within time limit running time correct/wrong/unverifiable classification of approximate out
Baselines: Gibbs-SAA BP-SAA XOR-SMC Lingeling-UAI10 Lingeling-HBFS Lingeling-D4 Lingeling-ADDMC Lingeling-SSTD
Builds on: CDCL MiniSAT ACE knowledge compiler XOR-SMC Sample Average Approximation
Closest papers by meaning
- Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration with Provable Guarantees (AAAI 2024 · similarity 0.94)
- Towards Real-Time Approximate Counting (AAAI 2025 · similarity 0.85)
- An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes (AAAI 2024 · similarity 0.84)
- Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · similarity 0.84)
- An Approximate Skolem Function Counter (AAAI 2024 · similarity 0.84)
- Unifying Decision and Function Queries in Stochastic Boolean Satisfiability (AAAI 2024 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.