Probabilistic-bit Guided CDCL for SAT Solving using Ising Consensus Assumptions Melki Bino
arXiv:2605.04033v1 [cs.CR] 5 May 2026
Department of Electrical & Computer Engineering University of Texas at Dallas, Richardson, USA Email: [email protected]
Abstract—Boolean satisfiability (SAT) solvers are widely used in hardware verification, cryptanalysis, automatic test-pattern generation, and side-channel reasoning workflows. Modern conflictdriven 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. Index Terms—Boolean Satisfiability, CDCL, p-bit, Ising machine, Probabilistic Computing, Machine Learning, Hardware Security.
p-bit Engine
CPUs Phase Input
Backbone Guidelines
CDCL Threads
Fig. 1. Proposed p-bit-guided CDCL flow The p-bit Ising sampler produces low-violation candidate assignments whose stable consensus literals are passed to the CDCL solver as hard assumptions, which can reduce the initial CDCL subproblem. Soundness comes from CDCL checking plus unrestricted rescue fallback, not from the p-bit phase.
This paper studies a hybrid SAT-solving framework based on probabilistic bits (p-bits) and Ising sampling, as shown in Fig. 1. A CNF formula is mapped to an Ising-style energy function in which low-energy states correspond to assignments that violate few clauses. Multiple stochastic p-bit replicas are sampled, and high-agreement literals from low-violation samples are passed to CDCL as temporary assumptions. CDCL then solves the reduced subproblem under these assumptions using a bounded attempt-and-retry protocol. The p-bit stage is heuristic and is not used as a certificate of satisfiability or unsatisfiability. Correctness is preserved because every candidate result is checked by CDCL, and the solver can fall back to unrestricted CDCL when the p-bit assumptions are unproductive.
I. I NTRODUCTION Boolean satisfiability (SAT) asks whether a Boolean formula has an assignment that satisfies all of its clauses. Although SAT is NP-complete, modern conflict-driven clause-learning (CDCL) solvers can solve many large practical instances and are widely used in hardware verification, bounded model checking, equivalence checking, automatic test-pattern generation, cryptanalysis, and hardware-security analysis [1], [2]. In security-oriented applications, SAT formulations appear in logic-locking attacks, key recovery, hardware Trojan analysis [3], and side-channel constraint solving [4], [5]. In these settings, satisfying assignments are often meaningful artifacts, such as secret keys, counterexample traces, test patterns, or leakage-consistent internal states. CDCL solvers search through the Boolean assignment space using decisions, unit propagation, conflict analysis, clause learning, and non-chronological backtracking [6]. These mechanisms make CDCL highly robust, but satisfiable instances can still require many conflicts and propagations before the solver reaches a productive region of the search space. This motivates auxiliary guidance mechanisms that can propose partial assignments likely to agree with a satisfying assignment, while leaving final correctness to the CDCL solver.
We evaluate the framework on selected satisfiable benchmark families from SATLIB [7], including random 3-SAT instances (RTI), backbone-minimal sub-instances (BMS), and controlledbackbone random 3-SAT instances (CBS). The RTI family contains satisfiable random 3-SAT instances with fixed numbers of variables and clauses, while the BMS family contains corresponding backbone-minimal sub-instances generated by removing clauses without changing the backbone. The CBS family contains satisfiable random 3-SAT instances with controlled backbone sizes, allowing the effect of backbone structure on solver guidance to be studied systematically. Our results show that p-bit-derived CDCL assumptions can substantially reduce CDCL conflict and propagation counters on selected RTI and CBS benchmark families. However, the benefit is distribution-sensitive. The method is less effective on
1
some structured or transformed instances, and BMS improvements are partly influenced by retry and rescue-path behavior rather than by assumption guidance alone. We therefore present the proposed method as a study of p-bit-guided CDCL search effort, rather than as a claim of universal SAT-solver acceleration. Our contributions are summarized as follows: • We present a p-bit/Ising-assisted CDCL pipeline in which stochastic samples generate temporary assumptions for a conventional CDCL solver. • We formulate the guidance mechanism using clause-violation energy, sample agreement, magnetization, and conditional CDCL search reduction. • We evaluate the method on selected satisfiable SATLIB families, including RTI, BMS, and CBS benchmarks, and show that p-bit guidance can reduce CDCL conflict and propagation counters on selected RTI and CBS instances. • We characterize distribution-sensitive behavior and identify cases where improvements arise from retry or rescue-path effects rather than direct assumption quality. • We report exploratory suitability-gating results and identify feature leakage sources that must be removed before deployment-level evaluation. The paper is organized as follows. Section II presents relevant preliminaries and literature context, Section III develops the p-bit/Ising-assisted CDCL pipeline, Section IV presents the experiments, and Section V the conclusion.
[18]. Glucose introduced learned-clause quality metrics based on literal block distance (LBD) [19]. CaDiCaL incorporates modern preprocessing, inprocessing, simplification, and restart strategies [20], [21]. These techniques make CDCL solvers highly robust, but satisfiable instances may still require many conflicts and propagations before a useful region of the search space is reached. This motivates external guidance mechanisms that can provide promising partial assignments while preserving CDCL as the final correctness-preserving engine. Assumption-Based Solving. Most modern SAT solvers support solving under assumptions. Given a CNF formula F and a set of literals A = {a1 , . . . , ak }, the solver checks the satisfiability of F ∧ a1 ∧ · · · ∧ ak . (3) The assumptions are temporary: they restrict the current solver call but are not permanently added as clauses to the formula. If the formula is satisfiable under the assumptions, the returned assignment also satisfies the original formula F . If the formula is unsatisfiable under the assumptions, this does not imply that F itself is unsatisfiable; it only shows that no satisfying assignment exists within the subspace selected by A. Therefore, assumption-based guidance must include a fallback or retry mechanism when the assumptions are incorrect or too restrictive. This work uses the assumption interface as the connection between the p-bit sampler and CDCL. The p-bit stage proposes literals that appear stable across low-violation samples, and CDCL tests those literals as temporary assumptions. Thus, the stochastic sampler guides the search subspace, but it does not replace conflict analysis, clause learning, or satisfiability checking. p-bits and Ising-Style Sampling. A probabilistic bit, or pbit, is a binary stochastic unit that fluctuates between two states according to a tunable bias. Networks of interacting p-bits can be used to sample from Ising-like energy landscapes. In an Ising formulation, binary variables are represented as spins si ∈ {−1, +1}, and candidate assignments are assigned an energy. Lower energy typically corresponds to better agreement with the encoded constraints. For SAT, a CNF formula can be mapped to an energy function in which violated clauses contribute penalties. A simple conceptual form is X E(s) = 1{Cj is violated by s}, (4)
II. P RELIMINARIES CDCL SAT Solving. Boolean satisfiability (SAT) asks whether a Boolean formula admits an assignment that satisfies all clauses. Modern SAT solvers are largely based on conflictdriven clause learning (CDCL), which extends the DPLL procedure with conflict analysis, learned clauses, and nonchronological backtracking [6], [17]. A CDCL solver maintains a partial assignment over Boolean variables. At each step, the solver makes branching decisions, applies Boolean constraint propagation (BCP), detects conflicts when a clause becomes falsified, analyzes the implication graph, and learns a new clause that prevents the same conflicting assignment from being revisited. Two useful indicators of CDCL search effort are the number of conflicts and the number of propagated literals. We denote the conflict count by X Nconf = 1{iteration t derives a conflict}, (1)
Cj ∈F
t
and the propagation count by X Nprop = #{literals assigned by BCP at iteration t}. (2)
where each spin assignment s corresponds to a Boolean assignment. Assignments with smaller E(s) violate fewer clauses and are therefore closer to satisfying the formula. The p-bit sampler repeatedly explores this energy landscape and produces a collection of candidate assignments. Literals that take the same value across many low-violation samples are treated as high-agreement literals and are passed to CDCL as temporary assumptions. This approach is heuristic. Low energy does not guarantee satisfiability, and high agreement does not guarantee that a literal belongs to a satisfying assignment. However, when the Ising landscape correlates well with the satisfying region, these
t
These expressions are conceptual summaries of solver activity. In the experiments, we use the accumulated solver-reported counters obtained through CaDiCaL/PySAT, including counters accumulated during retry and rescue phases when those phases are invoked. Practical CDCL performance depends not only on the highlevel search procedure but also on several implementation and heuristic choices. MiniSat popularized efficient watchedliteral propagation, activity-based branching, and phase saving
2
TABLE I C OMPARISON WITH RELATED SAT- GUIDANCE AND I SING - BASED SOLVING APPROACHES . Approach
Guidance / Solver Role
Platform
Benchmarks
GNN-Core Guidance [8] Fourier Warm Start [9] Electronic Ising SLS [10] GNN Backbone Hints [11] FPGA p-bit Ising [12] GPU CLS Warm Start [13] Finite-Field Guidance [14] Circuit-Aware GNN [15] Structured Ising SAT [16] This work
UNSAT-core scores for VSIDS Continuous relaxation for CDCL warm start Ising-based standalone SLS Backbone-based phase hints Standalone p-bit Ising solver Parallel CLS for CDCL warm start Finite-field optimization before CDCL Phase hints and clause filtering Standalone Ising formulation p-bit literals as CDCL assumptions
SW/GPU CPU/GPU Ising chip SW/GPU FPGA GPU+CPU GPU+CPU SW/GPU Ising/SW SW
SAT Competition Hybrid Boolean constraints Random 3-SAT, Circuit-SAT SAT Competition 3R3X SAT Cardinality, graph problems SAT Competition 2024 LEC circuit benchmarks Factorization SAT Selected SATLIB
Complete
Gate
✓ P – ✓ – P P ✓ – ✓
– – – – – – – – – Expl.
Notes: “Complete” indicates whether the overall method preserves SAT/UNSAT correctness through a complete CDCL procedure. “Gate” indicates whether a learned suitability classifier is used to decide when guidance is applied; Expl. marks the leakage-contaminated exploratory gate in this artifact. P denotes partial completeness or completeness only through a CDCL fallback stage.
literals can reduce the CDCL search space and lower the number of conflicts and propagations. When the landscape is misleading, the assumptions may hurt performance; for this reason, our framework includes retry and unrestricted fallback. Parallel and Learning-Augmented SAT. Prior work has explored several ways to improve SAT solving beyond a single sequential CDCL search. Parallel SAT solvers use portfolio strategies, where multiple solvers run with different heuristics, or divide-and-conquer strategies, where the search space is partitioned into subproblems [22]. GPU-based approaches have attempted to accelerate propagation, local search, or simplification by using parallel hardware [23], [24]. Machine-learning-guided SAT methods use learned models to predict useful solver information. Examples include satisfiability prediction, variable branching guidance, phase selection, backbone prediction, unsatisfiable-core prediction, and learned clause management [11], [25], [26]. Other methods use continuous or differentiable relaxations to produce warm starts or candidate assignments for SAT solving [9], [27], [28]. These methods differ in how strongly they modify the underlying solver. Some change branching or phase heuristics, some warmstart CDCL, and some operate as standalone incomplete search procedures. The proposed framework is closest in spirit to methods that generate auxiliary guidance for CDCL. However, our guidance is obtained from p-bit/Ising samples and is applied through the solver’s assumption interface. CDCL remains solely responsible for validating assignments and proving unsatisfiability. This distinction is important because the p-bit phase is not complete and does not provide a proof certificate by itself. Security-Motivated SAT. SAT is widely used in cryptography and hardware security because bit-level systems can often be encoded naturally as CNF formulas. In cryptanalysis, satisfying assignments may correspond to secret keys, preimages, or internal cipher states [29]. In logic-locking attacks, SAT solvers search for discriminating input patterns and key assignments that distinguish candidate locked circuits [30]. In automatic test-pattern generation and Trojan analysis, SAT constraints can encode activation conditions, propagation paths, and structural circuit properties. Side-channel reasoning can also be formulated as a constraint-solving problem when observed leakage
restricts the set of possible internal states [31], [32]. These applications motivate hybrid witness-search methods that reduce the number of conflicts and propagations needed to find satisfying assignments. However, security-derived SAT instances may be structurally different from random SAT benchmarks. Cryptographic formulas often contain XOR-like parity relations, strong diffusion, equivalent keys, and many symmetric or near-symmetric assignments. Side-channel constraints may be noisy, probabilistic (often modeled as random circuit learning [33]), or trace-ranked rather than clean hard clauses. Such properties can weaken the usefulness of highagreement literals: a sampler may fail to produce stable literal values, or the stable values may not correspond to globally useful CDCL assumptions. Therefore, the present work should be viewed as a step toward p-bit-guided SAT solving, with security-domain validation left as future work. Comparison with Related Work. Table I compares the proposed method with representative Ising-based, learningguided, and hybrid SAT-solving approaches. Existing work has explored GNN-based branching or backbone guidance, continuous relaxations for warm starting CDCL, electronic or FPGA Ising machines, GPU-based continuous local search, and circuit-aware learned phase guidance. These methods differ in three important dimensions: whether the guidance is used inside CDCL or as a standalone solver, whether SAT/UNSAT correctness is preserved by a complete CDCL fallback, and whether the method learns when guidance should be applied. The present work occupies a specific point in this design space. It uses p-bit-derived literals as temporary CDCL assumptions, retains CDCL as the correctness-preserving backend, and studies an exploratory suitability gate for deciding when hybrid guidance should be invoked. Unlike hardware-accelerated or GPU-optimized approaches, our current implementation is a Python prototype and is evaluated using CDCL internal counters rather than wall-clock speedup. The goal of this study is therefore to evaluate whether p-bit-derived assumptions can reduce CDCL search effort, not to claim end-to-end runtime acceleration.
3
ML Classifier Hybrid SAT Solver
Pure SAT Solver
Fig. 2. Hybrid CDCL flow. The input CNF is encoded as a quadratic Ising Hamiltonian. The p-bit engine anneals R stochastic replicas from high to low temperature, and the resulting samples are ranked by their direct CNF violation counts. High-agreement literals from the best-ranked samples are passed to CDCL as temporary assumptions. A budget-limited attempt-and-retry stage is followed by unrestricted CDCL fallback, preserving completeness. An optional suitability gate, trained offline, determines whether a formula should use the hybrid path.
III. P ROBABILISTIC - BIT I SING G UIDANCE
field. With the sign convention used by the implementation, the effective local field is X ℓ̃i = −hi − Jij yj , (10)
A. From CNF to Ising Energy Let the input CNF formula be m ^ F (x) = Ca (x),
j
and the update probability is 1 1 + tanh(β ℓ̃i ) . (11) 2 The inverse temperature β is annealed from a hot exploratory setting to a cold exploitative setting, and R independent replicas are sampled. The replicas are ranked by V (s) instead of raw Ising energy because quadratization penalties can affect auxiliary variables in ways that are not directly relevant to the original CNF clauses. High-agreement literals. Let T denote the top-k replicas with the smallest direct CNF violation counts. For each original variable, we compute the top-sample agreement score 1 X (r) (k) s̄i = si . (12) k
(5)
Pr(yi = +1 | y\i ) =
a=1
where xi ∈ {0, 1} and each clause Ca is a disjunction of literals. We map Boolean variables to spin variables si ∈ {−1, +1} using si = 2xi − 1. For each clause, we define a violation indicator ( 1, Ca (s) is falsified, va (s) = 0, Ca (s) is satisfied. The total violation count is then m X V (s) = va (s),
(6)
(7)
r∈T
(8)
Variable i is selected as a high-agreement candidate when (k) |s̄i | = 1, meaning that all top-k samples assign the same value to that variable. We avoid referring to these literals as a backbone, because backbone information is a benchmark property and is not available to the sampler. The selected candidates are further ranked using a qualityweighted magnetization score, R X (1 + V (s(r) ))−1 (r) mi = wr si , wr = P . (13) (q) ))−1 q (1 + V (s r=1
a=1
where V (s) = 0 if and only if s satisfies the original CNF formula. The implementation constructs a quadratic Ising Hamiltonian of the form 1 y = [s; z], (9) E(y) = E0 + h⊤ y + y ⊤ Jy, 2 where z denotes auxiliary spins introduced by the Rosenberg quadratization of higher-order clause penalties. The resulting Ising model is used as a stochastic search landscape rather than as an exact Gibbs sampler. Candidate assignments are evaluated using the direct violation count V (s) computed on the original DIMACS clauses and original variables. Thus, auxiliary spins influence the annealing trajectory, but they are not counted when ranking samples for CDCL guidance.
This weighting gives a larger influence to samples that violate fewer original CNF clauses. The top-H ranked candidates are converted back to SAT literals and form the assumption set ρpbit = {ℓ1 , . . . , ℓH }.
(14)
This set is then passed to the CDCL solver through its assumption interface. Attempt, retry, and fallback. The hybrid solver first invokes CDCL under the p-bit-derived assumption set ρpbit with a conflict budget B1 . If this attempt exhausts its budget or the assumptions lead to an unsatisfiable restricted subproblem, the
B. p-bit Sampling and Assumption Selection p-bit update rule. A p-bit is a tunable stochastic binary unit. During sampling, each spin is updated according to its local
4
TABLE II SATLIB SELECTED BENCHMARK IMPROVEMENTS . Benchmark #Vars #Clauses Ratio
CBS
RTI BMS
100 100 100 100 100 100 100 100 100 100
403 411 418 423 429 435 441 449 429 429
4.03 4.11 4.18 4.23 4.29 4.35 4.41 4.49 4.29 4.29
Conflicts Propagations Pure Hybrid Improve Pure Hybrid Improve 286.5 55.0 80.8% 6693.5 1289.5 80.7% 277.5 51.0 81.6% 6352.0 1236.5 80.5% 272.5 47.0 82.8% 6194.5 1087.0 82.5% 247.5 45.5 81.6% 5559.5 1103.0 80.2% 245.5 44.0 82.1% 5600.0 1063.5 81.0% 226.5 37.0 83.7% 5317.0 913.5 82.8% 235.0 34.0 85.5% 5370.5 825.5 84.6% 214.0 32.0 85.0% 4943.5 802.5 83.8% 259.5 43.0 83.4% 6012.0 1015.5 83.1% 650.5 404.5 37.8% 15742.5 9245.5 41.3%
solver retries with a second budget B2 . If both guided attempts fail, the framework switches to unrestricted CDCL without assumptions. This final fallback stage preserves completeness because the original formula is solved by a complete CDCL solver without any p-bit restrictions. The retry and fallback stages can also influence the measured solver counters. In particular, failed guided attempts may add learned clauses that are reused by the unrestricted fallback. Therefore, an observed improvement can come from two different mechanisms: direct pruning by useful p-bitderived assumptions, or indirect clause reuse during rescue. The experiments distinguish these effects when interpreting benchmark-dependent behavior. Why p-bit-Derived Assumptions Can Help. Let S denote the set of satisfying assignments of the CNF formula. If the p-bit-derived assumption set ρpbit agrees with at least one satisfying assignment x∗ ∈ S, then CDCL searches a restricted subcube, Ω(ρpbit ) = {x ∈ {0, 1}n : x |= ρpbit },
hybrid method reduces both conflicts and propagations by at least 20%. Gate architecture. The intended deployment architecture is a pre-solve classifier that uses only features computable from the CNF formula before solving. We also consider a probe-based variant that augments structural CNF features with statistics from a short, low-cost p-bit sampling run. In this artifact, the probe consists of 10 samples and 200 sweeps. The reported gate results should be interpreted as diagnostic rather than deployment-ready. The models are trained using a 70/30 formula-level in-distribution split over selected SATLIB configurations, and the feature set contains leakage sources identified in the experimental analysis. Therefore, the current gate results are best viewed as an upper-bound indication that hybrid suitability may be learnable, not as a validated classifier for unseen benchmark families. Agreement statistic. The main probe statistic is the mean absolute weighted magnetization, n 1X |mi |. (17) qabs = n i=1
(15)
n−|ρpbit |
whose size is 2 before propagation. Boolean constraint propagation can further extend the assumption set by implying additional assignments, producing a smaller effective search region. When the assumptions are consistent with a useful solution basin and trigger productive propagation chains, CDCL may explore fewer inconsistent branches. This can reduce both the conflict count Nconf and the propagation count Nprop . This reduction is not guaranteed. If the p-bit-derived assumptions are inconsistent with all satisfying assignments, or if they guide CDCL into a difficult region of the search space, the solver may spend additional effort before recovering. The attempt, retry, and fallback protocol is therefore necessary: it allows the framework to exploit helpful assumptions while still recovering from misleading ones.
This statistic summarizes how strongly the p-bit samples polarize across variables. In this paper we denote it by qabs to avoid confusion with the squared Edwards–Anderson order parameter. A large qabs indicates strong sample agreement, but it is not sufficient to guarantee useful CDCL assumptions. For example, some instance families can produce highly polarized p-bit samples while still yielding poor hybrid performance. This shows that agreement strength and guidance quality are related but distinct quantities, motivating the use of a learned suitability gate rather than a fixed agreement threshold. IV. E XPERIMENTS
C. Hybrid Suitability Gate
A. Experimental Setup
Label definition. Because p-bit guidance is distributionsensitive, the framework also studies a suitability gate that predicts whether the hybrid path should be used. For each formula, we define a strict binary label Ch Ph y =1 1− ≥ 0.20 ∧ 1 − ≥ 0.20 , (16) Cp Pp where Cp and Pp are the pure-CDCL conflict and propagation counts, and Ch and Ph are the corresponding hybrid medians over random seeds. A formula is labeled as suitable only if the
We evaluate the proposed p-bit-guided CDCL framework on selected satisfiable benchmark families from SATLIB [7]. The benchmark set contains 4,800 CNF formulas drawn from five families: controlled-backbone random 3-SAT (CBS), random 3-SAT instances (RTI), backbone-minimal sub-instances (BMS), flat graph-coloring instances (flat), and small-world graph-coloring instances (sw). The CBS subset contains 4,000 formulas across 40 parameter configurations, with all CBS instances having n = 100 variables. The RTI and BMS subsets
5
Pure Hybrid
300
Pure Hybrid
Propagations
Conflicts
400
200 100 4.1
4.2
4.3
4.4
4.5
ratio α
20
40
60
80
Pure Hybrid
8000 6000 4000 2000 4.1
backbone size b
Pure Hybrid
4.2
4.3
4.4
4.5
ratio α
20
40
60
80
backbone size b
(a) (b) Fig. 3. Conflict and propagation reduction trends. Pure and hybrid CDCL counters are averaged over CBS configurations as a function of clause density α = m/n and controlled backbone size b. All CBS instances have n = 100 variables. The hybrid method consistently reduces both median conflicts and median propagations across the evaluated parameter sweep.
each contain 100 formulas, while the flat and sw graph-coloring subsets each contain 300 formulas. The experiments were performed on a machine with an Intel Core Ultra 7 258V processor. The processor has 8 physical cores, one hardware thread per core, a maximum clock frequency of 4.8 GHz, 14 MiB aggregate L2 cache, and 12 MiB L3 cache. All experiments were run on an x86 64 Linux environment. The SAT backend is CaDiCaL accessed through PySAT. Each formula is solved once using pure CDCL and five times using the hybrid p-bit-guided CDCL configuration with different random seeds. The hybrid configuration uses R = 30 p-bit samples, 700 annealing sweeps, top-5 sample agreement, at most H = 12 CDCL assumptions, an initial guided conflict budget of B1 = 1500, a retry budget of B2 = 1000, and unrestricted CDCL fallback. Unless otherwise stated, hybrid results are reported as medians over the five random seeds. The primary metrics are the accumulated CaDiCaL conflict and propagation counters. These counters include work performed during guided attempts, retries, and unrestricted fallback when fallback is invoked. We focus on solver-internal counters rather than wall-clock time because the current p-bit sampler is a Python prototype and its implementation overhead would obscure the algorithmic effect of the proposed guidance mechanism. For the suitability-gate experiments, we use a 70/30 formulalevel in-distribution train/test split stratified within SATLIB configuration groups. Thus, formulas from the same SATLIB configuration may appear in both training and testing sets. Cross-family tests are reported separately to evaluate generalization under distribution shift.
requires median conflict counts between 214 and 286.5, while the hybrid method reduces these medians to between 32 and 55. This corresponds to conflict reductions of 80.8%–85.5%. Median propagation counts are reduced from 4943.5–6693.5 to 802.5–1289.5, corresponding to propagation reductions of 80.2%–84.6%. The RTI family shows a similar trend, with an 83.4% median conflict reduction and an 83.1% median propagation reduction. These results indicate that p-bit-derived assumptions can substantially reduce CDCL search effort on selected satisfiable random and controlled-backbone 3-SAT instances. Figures 3a and 3b show the CBS trends as a function of clause density α = m/n and controlled backbone size b. For the evaluated CBS configurations, the hybrid curve remains consistently below the pure-CDCL curve for both conflicts and propagations. This suggests that, within these selected CBS settings, p-bit-derived assumptions often guide CDCL toward productive regions of the search space. The BMS family shows more moderate aggregate improvement, with a 37.8% median conflict reduction and a 41.3% median propagation reduction. However, the median rescue rate for BMS is 1.0. Therefore, at least half of the BMS formulas route all five hybrid seeds to unrestricted rescue rather than being solved during the assumption-guided attempts. This indicates that the BMS improvement should not be attributed solely to direct p-bit assumption quality. Instead, it is consistent with a warm-restart effect, where CDCL reuses learned clauses generated during failed guided attempts. A separate attribution baseline is needed to isolate this effect. The graph-coloring families are less favorable to the proposed guidance mechanism. The flat graph-coloring family has a 48.3% hybrid-good rate and a 22.8% median conflict reduction. The sw family is a stronger failure case: it has only a 15.7% hybrid-good rate, 0.0% median conflict reduction, and −1.8% median propagation reduction. Thus, on sw instances, the hybrid method slightly increases the median propagation count. Interestingly, sw instances have the highest median agreement statistic, qabs = 0.638, among the evaluated families. This shows that strong p-bit sample polarization alone does not guarantee useful CDCL assumptions.
TABLE III FAMILY- LEVEL SUMMARY OF HYBRID SUCCESS . Family CBS RTI BMS flat sw
Good 85.6% 82.0% 63.0% 48.3% 15.7%
Conf. 81.5% 82.5% 39.6% 22.8% 0.0%
Prop. Rescue 79.6% 0.0% 79.9% 0.0% 39.8% 100.0% 19.2% 0.0% -1.8% 0.0%
B. SATLIB Family-Level Behavior
C. Classifier-Gated Hybrid Solving
Table II summarizes the median conflict and propagation counts for selected CBS clause-density buckets, together with RTI and BMS results. Across the CBS families, pure CDCL
Because p-bit guidance is highly distribution-sensitive, we also evaluate learned suitability gates that decide whether a formula should be routed to the hybrid solver or to pure CDCL.
6
TABLE IV L EAKAGE - CONTAMINATED DIAGNOSTIC GATE SUMMARY.
[7] H. H. Hoos and T. Stützle, “Satlib: An online resource for research on sat,” Sat, vol. 2000, pp. 283–292, 2000. [8] D. Selsam and N. Bjørner, “Guiding high-performance sat solvers with unsat-core predictions,” in Theory and Applications of Satisfiability Testing – SAT 2019, vol. 11628 of Lecture Notes in Computer Science, pp. 336–353, Springer, 2019. [9] A. Kyrillidis, A. Shrivastava, M. Vardi, and Z. Zhang, “FourierSAT: A Fourier expansion-based algebraic framework for solving hybrid boolean constraints,” AAAI Conf. on Artificial Intelligence (AAAI), 2020. [10] A. Sharma, M. Burns, A. Hahn, and M. Huang, “Augmenting an electronic ising machine to effectively solve boolean satisfiability,” Scientific Reports, vol. 13, no. 1, p. 22858, 2023. [11] W. Wang, Y. Hu, M. Tiwari, S. Khurshid, K. McMillan, and R. Miikkulainen, “NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks,” Int’l Conf. on Learning Representations (ICLR), 2024. [12] S. Nikhar, S. Kannan, N. A. Aadit, S. Chowdhury, and K. Y. Camsari, “All-to-all reconfigurability with sparse and higher-order ising machines,” Nature Communications, vol. 15, p. 8977, 2024. [13] Y. Cen, Z. Zhang, and X. Fong, “Massively parallel continuous local search for hybrid sat solving on gpus,” in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 39, pp. 11140–11149, 2025. [14] C. Kim, C. Portner, M. Liu, S. Dai, H. Ren, B. Khailany, A. Velasquez, I. Alkhouri, and C. Yu, “Galoissat: Differentiable boolean satisfiability solving via finite field algebra,” 2026. [15] J. Zhu, Z. Zheng, Z. Shi, Y. Cai, and Q. Xu, “Circuit-aware sat solving: Guiding cdcl via conditional probabilities,” 2025. [16] Anonymous, “On solving structured sat on ising machines: A semiprime factorization study,” 2025. Metadata should be verified before submission. [17] M. Davis, G. Logemann, and D. Loveland, “A machine program for theorem proving,” Communications of the ACM, vol. 5, no. 7, 1962. [18] N. Eén and N. Sörensson, “An Extensible SAT-solver,” Int’l Conf. on Theory and Applications of Satisfiability Testing (SAT), 2003. [19] G. Audemard and L. Simon, “Predicting Learnt Clauses Quality in Modern SAT Solvers,” Int’l Joint Conf. on Artificial Intelligence (IJCAI), 2009. [20] A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt, “CaDiCaL 2.0,” Int’l Conf. on Computer-Aided Verification (CAV), 2024. [21] A. Biere, “CaDiCaL SAT Solver, Version 1.9.5.” https://github.com/ arminbiere/cadical, 2022. [22] C. Le Frioux, E. Hebrard, B. Mazure, and L. Sais, “Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework,” Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2019. [23] M. Osama, A. Wijs, and A. Biere, “SAT Solving with GPU Accelerated Inprocessing,” Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2021. [24] H. Fujii and N. Fujimoto, “GPU Acceleration of BCP Procedure for SAT Algorithms,” Int’l Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA), 2012. [25] D. Selsam, M. Lamm, B. Bünz, P. Liang, L. de Moura, and D. L. Dill, “Learning a SAT Solver from Single-Bit Supervision,” Int’l Conf. on Learning Representations (ICLR), 2019. [26] D. Selsam and N. Bjørner, “Guiding High-Performance SAT Solvers with Unsat-Core Predictions,” Int’l Conf. on Theory and Applications of Satisfiability Testing (SAT), 2019. [27] Y. Cen, Z. Zhang, and X. Fong, “Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs,” AAAI Conf. on Artificial Intelligence (AAAI), 2025. [28] Y. Zhang, H.-L. Zhen, M. Yuan, and B. Yu, “DiffSAT: Differential MaxSAT Layer for SAT Solving,” Int’l Conf. on Computer-Aided Design (ICCAD), 2024. [29] M. Soos, K. Nohl, and C. Castelluccia, “Extending SAT Solvers to Cryptographic Problems,” in International Conference on Theory and Applications of Satisfiability Testing, pp. 244–257, Springer, 2009. [30] P. Subramanyan, S. Ray, and S. Malik, “Evaluating the Security of Logic Encryption Algorithms,” in IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 137–143, IEEE, 2015. [31] P. Kocher, J. Jaffe, and B. Jun, “Differential Power Analysis,” in Annual International Cryptology Conference, pp. 388–397, Springer, 1999. [32] S. Mangard, E. Oswald, and T. Popp, Power Analysis Attacks: Revealing the Secrets of Smart Cards. Springer, 2007. [33] S. Ahmed and K. Shamsi, “On oracle-guided random circuit learning via stochastic boolean satisfiability,” in Proceedings of the 2026 Design, Automation & Test in Europe Conference (DATE), 2026.
Policy Apply Keep Avoid Conf. Prop. Always Hybrid 100.0% 100.0% 0.0% 67.6% 54.8% Probe RF 87.5% 94.8% 41.0% 67.4% 55.1% Two-Stage RF 87.3% 94.6% 41.0% 67.2% 54.0% Always Pure 0.0% 0.0% 100.0% 0.0% 0.0%
Table IV summarizes the gating results. The intended role of the gate is not necessarily to improve aggregate performance on a hybrid-friendly benchmark mixture, but to preserve the most beneficial hybrid applications while avoiding harmful ones, especially on families such as sw. The always-hybrid policy reduces total conflicts by 67.6% and total propagations by 54.8% relative to always-pure CDCL. This reflects the fact that the selected benchmark mixture is dominated by hybrid-friendly CBS instances. The randomforest ProbeGate achieves 83.9% accuracy, 86.3% precision, and 94.8% recall. It preserves 94.8% of hybrid wins while routing 87.5% of formulas to the hybrid path. The gate avoids 41.0% of hybrid-loss cases. However, these gating results should be interpreted as diagnostic rather than deployment-ready. The feature set contains Oracle-derived and benchmark metadata features, discussed below. Therefore, the reported gate performance is best viewed as a leakage-contaminated upper bound on the learnability of hybrid suitability under the current experimental protocol. V. C ONCLUSION This paper studied a p-bit-guided CDCL framework that connects physics-inspired stochastic search with conventional SAT solving. The proposed method uses an Ising sampler to identify stable high-agreement literals, passes them to CDCL as temporary assumptions, and preserves correctness through unrestricted CDCL fallback. The exploratory ProbeGate results suggest that hybrid suitability may be learnable, but stricter evaluation is needed before deployment. Future work should remove feature-leakage sources, add attribution baselines, evaluate the method on broader SAT families and security-motivated CNFs, and extend the framework to quantified and constraintrich domains. R EFERENCES [1] A. Biere, M. Heule, H. van Maaren, and T. Walsh, eds., Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, IOS Press, 2021. [2] V. Ganesh and M. Y. Vardi, “On the Unreasonable Effectiveness of SAT Solvers,” in Beyond the Worst-Case Analysis of Algorithms, Cambridge University Press, 2021. [3] D. Jain, S. Ahmed, G. Zhao, R. Datta, and K. Shamsi, “Trojan localization in generic ams circuits from combined power and functional queries,” in 2025 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 239–249, IEEE Computer Society, 2025. [4] K. Shamsi and Y. Jin, “Circuit deobfuscation from power side-channels using pseudo-boolean sat,” in 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), pp. 1–9, IEEE, 2021. [5] S. Ahmed, D. Jain, and K. Shamsi, “Improving error tolerance and scalability in pseudo-boolean sat-based generic side-channel analysis,” in 2025 IEEE International Test Conference (ITC), pp. 434–437, IEEE, 2025. [6] J. P. M. Silva and K. A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” Int’l Conf. on Computer-Aided Design (ICCAD), 1996.
7