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.

翻译：布尔可满足性（SAT）求解器广泛应用于硬件验证、密码分析、自动测试图案生成及侧信道推理工作流。现代冲突驱动子句学习（CDCL）求解器效率极高，但可满足实例在定位搜索空间的有效区域前，仍需进行大量冲突分析与布尔传播。本文研究一种混合SAT求解框架，其中概率比特（p-bit）伊辛采样器提出高一致性文字，并将其作为临时假设传递至CDCL。其目标并非替代CDCL，而是评估随机低违例采样能否在通过CDCL回退保持正确性的同时，降低CDCL内部搜索开销。在受控骨干随机3-SAT基准测试上，该混合方法相比纯CDCL将中位冲突数减少80.8-85.5%，中位传播次数减少80.2-84.6%。观察到的收益具有分布敏感性，表明p-bit引导仅对特定实例类别有效。我们进一步报告了用于估算何时可能受益于混合求解的探索性机器学习门控机制：在一次选定运行中，随机森林门控保留了94.8%的混合求解优势，表明轻量级门控有助于避免无成效的混合求解调用。