Probabilistic-bit Guided CDCL for SAT Solving using Ising Consensus Assumptions
TLDR
A hybrid SAT solver uses a p-bit Ising sampler to guide CDCL, significantly reducing conflicts and propagations on specific 3-SAT benchmarks.
Key contributions
- Developed a hybrid SAT solver combining p-bit Ising sampling with CDCL for improved performance.
- P-bit sampler provides high-agreement literal assumptions to CDCL, reducing internal search effort.
- Achieved 80%+ reduction in conflicts and propagations on controlled-backbone random 3-SAT instances.
- Explored machine learning gates to estimate when hybrid solving is most effective, retaining 94.8% of wins.
Why it matters
This paper introduces a novel hybrid approach that significantly boosts CDCL SAT solver efficiency by guiding it with a p-bit Ising sampler. It demonstrates substantial reductions in search effort on specific problem classes, enhancing SAT solving in critical applications. The use of ML gates to predict utility further improves practical applicability.
Original Abstract
Boolean satisfiability (SAT) solvers are widely used in hardware verification, cryptanalysis, automatic test-pattern generation, and side-channel reasoning workflows. Modern conflict-driven clause-learning (CDCL) solvers are highly effective, but satisfiable instances may still require substantial conflict analysis and Boolean propagation before identifying productive regions of the search space. This paper studies a hybrid SAT-solving framework in which a probabilistic-bit (p-bit) Ising sampler proposes high-agreement literals that are passed to CDCL as temporary assumptions. The goal is not to replace CDCL, but to evaluate whether stochastic low-violation samples can reduce CDCL internal search effort while retaining correctness through CDCL fallback. On selected controlled-backbone random 3-SAT benchmarks, the hybrid method reduces median conflicts by 80.8-85.5% and median propagations by 80.2-84.6% relative to pure CDCL. The observed benefit is distribution-sensitive, suggesting that p-bit guidance is effective only for certain instance classes. We further report exploratory machine-learning gates that estimate when hybrid solving is likely to help. On the selected run, a random-forest gate retains 94.8% of hybrid wins, indicating that lightweight gating may help avoid unproductive hybrid calls.
📬 Weekly AI Paper Digest
Get the top 10 AI/ML arXiv papers from the week — summarized, scored, and delivered to your inbox every Monday.