cs.AIOct 30, 2026

SAT-ACT: Learning CDCL Branching from Outcome-Derived Action Preferences

Authors: Zhenchao Sun, Chongyang Tao, Ping Lu, Tongkai Lu, Jianling Gao, Shuai Ma

Organizations: SKLCCSE Lab, Beihang University, Beijing, China

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Learning-based approaches have increasingly been explored for SAT solving, with particular attention to improving branching decisions in conflict-driven clause learning (CDCL) solvers. These approaches derive branching guidance either from static structural properties of SAT formulas or from dynamic signals obtained through solver feedback and execution traces. However, these forms of supervision provide limited evidence about state-dependent branching effects, while different outcome measures may favor different branching choices. To address these limitations, we propose SAT-ACT, an outcome-derived learning framework for CDCL branching. We design three complementary outcome comparison criteria to extract action preferences from independent branching action rollouts initiated at the same solver state. The criteria identify preferences supported by the outcomes and leave comparisons unresolved when the evidence is insufficient or conflicting, instead of forcing an ordering using a predefined scalar metric. A state-conditioned network learns branching priorities from the extracted preferences and uses them to guide CDCL search directly without online action rollouts. We further introduce non-dominated heuristic action supervision, which retains the solver-selected action as a training target only when it remains non-dominated under these preferences. Solver-level experiments show that SAT-ACT consistently reduces CDCL search costs on three SAT families and improves PAR-2 on the SAT Competition benchmarks.

Figures & tables

Figure 1: Overview of SAT-ACT , an outcome-derived learning framework for CDCL branching. Candidate branching actions initiate independent CDCL rollouts from the same solver state. The rollout outcomes are compared to extract action preferences, which supervise a state-conditioned branching action network through pairwise ranking.
DatasetMethodsΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrowMRPP ↓\downarrowW(1%) ↑\uparrow
SRCaDiCaL ( 2024 )0.00%0.00%0.00%1.0000.00%
NeuroCore (3-call) ( 2019 )-32.61%-29.99%-33.38%0.66379.90%
NeuroCore (5-call) ( 2019 )-38.44%-35.29%-39.34%0.60284.30%
GQSAT (3-call) ( 2020 )-20.74%-18.40%-20.64%0.80068.90%
GQSAT (5-call) ( 2020 )-24.36%-21.80%-24.03%0.77470.80%
SATformer ( 2023 )-12.22%-11.52%-13.02%1.00024.40%
Table 1: Solver-level comparison on SR, CA, and PS. Lower is better for ΔC\Delta_{C} , ΔD\Delta_{D} , ΔP\Delta_{P} , and MRPP, while higher is better for W(1%).
Figure 2: Effect of the neural intervention budget on SR, CA, and PS. Bars report relative changes in conflicts ( ΔC\Delta_{C} ), decisions ( ΔD\Delta_{D} ), and propagations ( ΔP\Delta_{P} ) with respect to native CaDiCaL.
CriteriaSRCAPS
 ΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrowΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrowΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrow
C1-30.89%-28.33%-31.87%-9.67%-4.43%-8.34%-30.99%-29.76%-28.99%
C1 + C2-39.23%-36.85%-38.39%-13.21%-8.05%-11.06%-34.32%-33.30%-31.97%
C1 + C2 + C3-41.49%-38.80%-40.30%-20.77%-14.30%-18.12%-36.55%-35.36%-34.24%
Table 2: Incremental analysis of outcome comparison criteria. Lower is better for all metrics.
VariantSRCAPS
 ΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrowΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrowΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrow
Pref. Only-41.49%-38.80%-40.30%-20.77%-14.30%-18.12%-36.55%-35.36%-34.24%
Heur. Only-30.84%-27.80%-31.91%-9.42%-3.03%-5.43%-16.30%-15.59%-13.41%
Pref. + Heur.-40.98%-38.13%-39.95%-17.52%-11.37%-13.58%-33.57%-32.65%-30.88%
Pref. + RG-42.32%-39.50%-41.85%-19.97%-13.83%-17.36%-36.97%-36.09%-35.36%
SAT-ACT-42.46%-39.63%-41.60%-20.85%-14.48%-18.63%-43.66%-42.55%-42.40%
Table 3: Ablation of heuristic action supervision strategies. Lower is better for all metrics.
Figure 3: Sensitivity to the heuristic action supervision weight on SR, CA, and PS under the 5-call setting. The panels report relative changes in propagations ( ΔP\Delta_{P} ) with respect to native CaDiCaL.
DatasetSolver#Solved#SAT#UNSAT#TimeoutPAR-2 (s)
SC-2023CaDiCaL (Native)2511161351494171.07
CaDiCaL ( SAT-ACT )2511151361494150.55
SC-2024CaDiCaL (Native)2641371271363989.14
CaDiCaL ( SAT-ACT )2661351311343952.30
SC-2025CaDiCaL (Native)2531441091474214.04
CaDiCaL ( SAT-ACT )2561431131444094.72
Table 4: Solver integration results on SAT Competition 2023–2025 instances. Solved is the sum of SAT and UNSAT results, and lower PAR-2 is better.
Appendix figures & tables7 assets

Supplementary material from the paper’s appendix.

Appendix

StatisticSRCAPS
Formula Statistics (Mean / Min / Max)
Variables119.78 / 40 / 200120.81 / 40 / 200118.70 / 40 / 200
Clauses652.90 / 159 / 1,2331,671.15 / 175 / 2,999823.15 / 224 / 1,599
Clause/Variable Ratio5.48 / 3.54 / 8.7213.64 / 4.38 / 15.006.93 / 5.13 / 8.00
Outcome-Derived Supervision
Instances20,00020,00020,000
Appendix
Table 5: Dataset and outcome-derived supervision statistics. CNF statistics are reported per instance. Decision states and rolled-out actions are reported after supervision filtering. A state is included only if it produces at least one preference pair. Rolled-out actions count candidate branching actions and exclude the additional unforced solver baseline. Criterion coverage is measured over all action pairs within these retained states, and the three criteria are not mutually exclusive.
DatasetBudgetSATUNSAT
  ΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrowΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrow
SR3-call-45.82%-36.35%-43.17%-33.70%-34.11%-34.08%
5-call-51.43%-41.42%-47.33%-37.34%-37.95%-37.88%
CA3-call-14.11%-7.23%-12.35%-6.77%-5.02%-4.65%
5-call-18.47%-9.46%-15.82%-23.87%-25.94%-22.95%
PS3-call-40.53%-37.10%-38.53%-26.68%-27.14%-23.72%
Appendix
Table 6: SAT and UNSAT subset analysis of SAT-ACT . Lower is better for all metrics.
DatasetComparison Criteria3-call5-call
  ΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrowΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrow
SRC1 + C2 + C3-36.84%-33.57%-36.45%-41.49%-38.80%-40.30%
w/o C1-26.66%-24.56%-26.00%-40.01%-37.55%-39.03%
w/o C2-29.71%-27.03%-30.00%-32.76%-30.81%-32.35%
w/o C3-28.85%-27.23%-28.76%-39.23%-36.85%-38.39%
C1 only-30.30%-27.60%-30.91%-30.89%-28.33%-31.87%
Appendix
Table 7: Leave-one-out analysis of outcome comparison criteria. Lower is better for all metrics.
Figure 4: Complete sensitivity analysis of the heuristic action supervision weight on SR, CA, and PS under the 5-call setting. The plots report relative changes in conflicts ( ΔC\Delta_{C} ), decisions ( ΔD\Delta_{D} ), and propagations ( ΔP\Delta_{P} ) with respect to native CaDiCaL; lower is better.
DatasetMethodΔC↓\Delta_{C}\downarrowΔD↓\Delta_{D}\downarrowΔP↓\Delta_{P}\downarrowMRPP ↓\downarrowW(1%) ↑\uparrow
SR HardCaDiCaL0.00%0.00%0.00%1.0000.00%
SAT-ACT (Pref. Only)-25.95%-25.28%-25.69%0.70478.10%
SAT-ACT-28.24%-27.44%-27.87%0.68081.40%
CA HardCaDiCaL0.00%0.00%0.00%1.0000.00%
SAT-ACT (Pref. Only)-1.99%-1.54%-0.68%1.00138.70%
SAT-ACT-3.72%-3.78%-3.22%1.00141.00%
Appendix
Table 8: Direct generalization of the same trained models used in the main experiments to the corresponding Hard splits. ΔC\Delta_{C} , ΔD\Delta_{D} , and ΔP\Delta_{P} denote relative changes in conflicts, decisions, and propagations, respectively. Lower is better for ΔC\Delta_{C} , ΔD\Delta_{D} , ΔP\Delta_{P} , and MRPP; higher is better for W(1%).
MethodBudgetInference (ms)
  SRCAPS
NeuroCore3-call29.665.937.2
NeuroCore5-call47.8109.258.3
GQSAT3-call66.1153.884.3
GQSAT5-call103.1251.2134.5
SATformerone-shot48.597.159.9
Appendix
Table 9: Neural inference cost of learning-based SAT branching methods. All values are average accumulated milliseconds per instance. Lower is better.
DatasetSolverNN Wait RatioNN Call Latency (s)
SC-2023CaDiCaL (Native)0.00%–
CaDiCaL ( SAT-ACT )11.99%9.61
SC-2024CaDiCaL (Native)0.00%–
CaDiCaL ( SAT-ACT )5.79%8.10
SC-2025CaDiCaL (Native)0.00%–
CaDiCaL ( SAT-ACT )7.92%8.43
Appendix
Table 10: Neural-call overhead for the SAT Competition evaluation.
More in this topic

Boolean Satisfiability

See all 25 papers

Explore similar work

CardsList
Mar 7, 2026

Learning to Rank the Initial Branching Order of SAT Solvers

Finding good branching orders is key to solving SAT problems efficiently, but finding such branching orders is a difficult problem. Using a learning based approach to predict a good branching order before solving, therefore, has potential. In this paper, we investigate predicting branching orders using graph neural networks as a preprocessing step to conflict-driven clause learning (CDCL) SAT solvers. We show that there are significant gains to be made in existing CDCL SAT solvers by providing a good initial branching. Further, we provide three labeling methods to find such initial branching orders in a tractable way. Finally, we train a graph neural network to predict these branching orders and show through our evaluations that a GNN-initialized ordering yields significant speedups on random 3-CNF and pseudo-industrial benchmarks, with generalization capabilities to instances much larger than the training set. However, we also find that the predictions fail at speeding up more difficult and industrial instances. We attribute this to the solver's dynamic heuristics, which rapidly overwrite the provided initialization, and to the complexity of these instances, making GNN prediction hard.

Arvid Eriksson, Gabriel Poesia, Roman Bresson +2

KTH Royal Institute of Technology · Kempner Institute at Harvard University · Mohamed Bin Zayed University of Artificial Intelligence

Boolean SatisfiabilityConstraint SatisfactionLearning to RankGraph Neural Networks
AskPDF
Oct 17, 2026

Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

Modern SAT solvers combine a rich repertoire of proof rules with sophisticated strategies that determine when and how to apply them. Often, the internal implementations are tightly coupled to particular strategies, making it inconvenient to define new strategies without changing solver internals. We present Tactix, a proof-producing sequential CDCL solver that incorporates a wide range of techniques in state-of-the-art solvers with a clean separation of proof rules from solving strategies. This separation enables a public interface through which users can invoke particular techniques, observe their effects, and program a wide range of solving strategies. The default strategy of Tactix is programmable over this interface and outperforms state-of-the-art solvers on benchmarks from the 2024--2026 SAT Competitions. We also use the interface to develop novel strategies tailored to challenging benchmarks from two application domains, which led to performance gains over strong baselines. We intend Tactix to serve as an infrastructure for designing and evaluating novel solving strategies. Finally, we also present a self-study of the AI-assisted development process behind Tactix.

Haoze Wu, André Schidler, Armin Biere +1

Amherst College, Amherst, MA, USA · University of Freiburg, Freiburg im Breisgau, Germany · Broadcom, Palo Alto, CA, USA

Boolean Satisfiability
AskPDF
May 15, 2026

Learning How to Cube

Despite the effectiveness of Cube-and-Conquer (C&C) for solving challenging Boolean Satisfiability (SAT) problems, no prior work has shown that transformer-based models can learn effective cubing heuristics. We introduce a neuro-symbolic post-training framework for this task. We design an MCTS-based data curation pipeline that uses symbolic heuristics to explore splitting decisions over SAT competition formulas, producing preference data grounded in solver statistics and augmented with reasoning traces from a teacher model. Our two-stage post-training, supervised fine-tuning (SFT) followed by direct preference optimization (DPO), enables a 4B-parameter model to achieve a pass@5 score of 53 on 100 SAT competition benchmarks, surpassing frontier LLMs such as Claude-Sonnet-4 (50) and matching the best symbolic heuristic (53). Ablations show that SFT alone improves pass@5 from 46 to 51, with DPO adding 2 additional benchmarks; an entropy/agreement ablation on realized first-cube decisions further shows that SFT, not DPO, accounts for the root-level decision diversity that produces complementary per-run coverage over deterministic symbolic methods. This demonstrates that transformers can be trained to make effective cubing decisions in a domain traditionally dominated by symbolic methods.

Ferhat Erata, Sam Kouteili, Thanos Typaldos +4

Yale University · AWS Agentic AI

TransformerConstraint SatisfactionNeurosymbolic LearningBoolean Satisfiability
AskPDF