Search papers, labs, and topics across Lattice.
This paper introduces a hybrid SAT-solving framework that combines conflict-driven clause-learning (CDCL) with a probabilistic-bit (p-bit) Ising sampler to guide the search process. The p-bit sampler proposes high-agreement literals as temporary assumptions to CDCL, aiming to reduce the solver's internal search effort. Experiments on controlled-backbone random 3-SAT benchmarks demonstrate that this hybrid approach can reduce median conflicts and propagations by over 80% compared to pure CDCL, with machine-learning gates showing promise in predicting when the hybrid approach will be beneficial.
Stochastic sampling from p-bit Ising models can slash the search effort of CDCL SAT solvers by over 80% on certain problem instances.
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.
