Research map / Learning theory and algorithms / Combinatorial and search optimization
Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration with Provable Guarantees
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 XOR-SMC, a polynomial algorithm with NP-oracle access that solves Satisfiability Modulo Counting problems by replacing model counting with XOR-constrained SAT, with constant-factor guarantees, and applies it to shelter placement and supply chain design.
Problem
Satisfiability Modulo Counting (SMC, NP^PP-complete) combines symbolic constraints with model-count predicates; prior solvers lack tight guarantees and perform suboptimally, especially with combinatorial constraints.
Approach
Approximate model counting thresholds via randomized XOR constraints (hashing) and majority voting over repeated SAT calls, encoding the whole procedure as a single SAT formula so SMC becomes SAT with a constant-approximation guarantee.
Key results
- On Hawaii shelter graphs, XOR-SMC ran in 0.04 hr, 0.11 hr and 0.16 hr versus 0.08-6.97 hr for sampler-based local search baselines, and found shelter placements with orders of magnitude more paths.
- On the real-world wheat supply network at 10%/20%/30% disaster scale, XOR-SMC achieved production of 232.2/210.2/147.8 tons versus best baseline values of 200.2/169.0/132.9 tons under a 2-hour limit for baselines.
- XOR-SMC is claimed to give constant multiplicative approximation guarantees with probability above 1-eta via a theorem based on XOR hashing and Chernoff bounds.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use XOR-SMC instead of local-search sampling baselines | Hawaii shelter placement · Hawaii shelter placement, N=121, N=183, and N=388 | running time: 0.04 hr vs 0.08 hr; 0.11 hr vs 0.17 hr; 0.16 hr vs 0.42 hr | Helped |
| Use XOR-SMC instead of local-search sampling baselines | Hawaii shelter placement · Hawaii shelter placement, different graphs | number of paths | Helped |
| Use XOR-SMC instead of SAA baselines | Small supply network · Small supply network, disaster scale 10% | production (tons): 86.5 -> 95.0 | Helped |
| Use XOR-SMC instead of SAA baselines | Small supply network · Small supply network, disaster scale 20% | production (tons): 95.4 -> 96.0 | Helped |
| Use XOR-SMC instead of SAA baselines | Small supply network · Small supply network, disaster scale 30% | production (tons): 118.8 -> 119.3 | Helped |
| Use XOR-SMC instead of SAA baselines | Real-world supply network · Real-world supply network, disaster scale 10% | production (tons): 187.2 -> 232.2 | Helped |
| Use XOR-SMC instead of SAA baselines | Real-world supply network · Real-world supply network, disaster scale 20% | production (tons): 143.7 -> 210.2 | Helped |
| Use XOR-SMC instead of SAA baselines | Real-world supply network · Real-world supply network, disaster scale 30% | production (tons): 132.9 -> 147.8 | Helped |
| Use XOR-SMC instead of SAA baselines | Small supply network · Small supply network, disaster scale 10% | running time: 0.67s vs 0.84s | Helped |
| Use XOR-SMC instead of SAA baselines | Small supply network · Small supply network, disaster scale 20% | running time: 1.19s vs 3.76s | Helped |
| Use XOR-SMC instead of SAA baselines | Small supply network · Small supply network, disaster scale 30% | running time: 17.63s vs 11.48s | Hurt |
| Use XOR-SMC instead of SAA baselines | Real-world supply network · Real-world supply network, disaster scale 10%, 20%, and 30% | running time: 57.8s, 75.5s, 96.9s vs 2 hr | Helped |
Limitations
- Guarantees hold only for the relaxed SMC formulation with implication instead of equivalence
- Number of repetitions T and parameter c depend on n, k and eta, and experiments use only T=2 heuristically
- Evaluation limited to two applied domains with small-to-moderate graph sizes
Experimental setup
Datasets: Hawaii Statewide GIS shelter map wheat supply chain network
Benchmarks: Hawaii shelter placement graphs (121, 183/186, 388 nodes) small synthetic supply network real-world wheat supply network
Metrics: number of paths to shelters total production (tons) running time
Baselines: GibbsSampler-LS QuickSampler-LS Unigen-LS BP-SAA Gibbs-SAA IS-SAA LoopyIS-SAA Weighted-SAA
Builds on: XOR-based approximate model counting Cook-Levin reduction SAT solving
Closest papers by meaning
- Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits (ICML 2025 · similarity 0.94)
- Learning Branching Heuristics for Propositional Model Counting (AAAI 2021 · similarity 0.85)
- Maximum Model Counting (AAAI 2017 · similarity 0.85)
- LLM-Guided Quantified SMT Solving over Uninterpreted Functions (AAAI 2026 · similarity 0.85)
- Unifying Decision and Function Queries in Stochastic Boolean Satisfiability (AAAI 2024 · similarity 0.83)
- An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes (AAAI 2024 · similarity 0.83)
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.