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

Zhenchao Sun; Chongyang Tao; Ping Lu; Tongkai Lu; Jianling Gao; Shuai Ma

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

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.

Dataset	Methods	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$	MRPP $\downarrow$	W(1%) $\uparrow$
SR	CaDiCaL ( 2024 )	0.00%	0.00%	0.00%	1.000	0.00%
	NeuroCore (3-call) ( 2019 )	-32.61%	-29.99%	-33.38%	0.663	79.90%
	NeuroCore (5-call) ( 2019 )	-38.44%	-35.29%	-39.34%	0.602	84.30%
	GQSAT (3-call) ( 2020 )	-20.74%	-18.40%	-20.64%	0.800	68.90%
	GQSAT (5-call) ( 2020 )	-24.36%	-21.80%	-24.03%	0.774	70.80%
	SATformer ( 2023 )	-12.22%	-11.52%	-13.02%	1.000	24.40%

Table 1: Solver-level comparison on SR, CA, and PS. Lower is better for

\Delta_{C}

\Delta_{D}

\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 (

\Delta_{C}

), decisions (

\Delta_{D}

), and propagations (

\Delta_{P}

) with respect to native CaDiCaL.

Criteria	SR			CA			PS
	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\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.

Variant	SR			CA			PS
	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\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 (

\Delta_{P}

) with respect to native CaDiCaL.

Dataset	Solver	#Solved	#SAT	#UNSAT	#Timeout	PAR-2 (s)
SC-2023	CaDiCaL (Native)	251	116	135	149	4171.07
SC-2023	CaDiCaL ( SAT-ACT )	251	115	136	149	4150.55
SC-2024	CaDiCaL (Native)	264	137	127	136	3989.14
SC-2024	CaDiCaL ( SAT-ACT )	266	135	131	134	3952.30
SC-2025	CaDiCaL (Native)	253	144	109	147	4214.04
SC-2025	CaDiCaL ( SAT-ACT )	256	143	113	144	4094.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

Formula Statistics (Mean / Min / Max)
Statistic	SR	CA	PS
Variables	119.78 / 40 / 200	120.81 / 40 / 200	118.70 / 40 / 200
Clauses	652.90 / 159 / 1,233	1,671.15 / 175 / 2,999	823.15 / 224 / 1,599
Clause/Variable Ratio	5.48 / 3.54 / 8.72	13.64 / 4.38 / 15.00	6.93 / 5.13 / 8.00
Outcome-Derived Supervision
Instances	20,000	20,000	20,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.

Dataset	Budget	SAT			UNSAT
		$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$
SR	3-call	-45.82%	-36.35%	-43.17%	-33.70%	-34.11%	-34.08%
SR	5-call	-51.43%	-41.42%	-47.33%	-37.34%	-37.95%	-37.88%
CA	3-call	-14.11%	-7.23%	-12.35%	-6.77%	-5.02%	-4.65%
CA	5-call	-18.47%	-9.46%	-15.82%	-23.87%	-25.94%	-22.95%
PS	3-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.

Dataset	Comparison Criteria	3-call			5-call
		$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$
SR	C1 + 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 (

\Delta_{C}

), decisions (

\Delta_{D}

), and propagations (

\Delta_{P}

) with respect to native CaDiCaL; lower is better.

Dataset	Method	$\Delta_{C}\downarrow$	$\Delta_{D}\downarrow$	$\Delta_{P}\downarrow$	MRPP $\downarrow$	W(1%) $\uparrow$
SR Hard	CaDiCaL	0.00%	0.00%	0.00%	1.000	0.00%
	SAT-ACT (Pref. Only)	-25.95%	-25.28%	-25.69%	0.704	78.10%
	SAT-ACT	-28.24%	-27.44%	-27.87%	0.680	81.40%
CA Hard	CaDiCaL	0.00%	0.00%	0.00%	1.000	0.00%
	SAT-ACT (Pref. Only)	-1.99%	-1.54%	-0.68%	1.001	38.70%
	SAT-ACT	-3.72%	-3.78%	-3.22%	1.001	41.00%

Appendix

Table 8: Direct generalization of the same trained models used in the main experiments to the corresponding Hard splits.

\Delta_{C}

\Delta_{D}

, and

\Delta_{P}

denote relative changes in conflicts, decisions, and propagations, respectively. Lower is better for

\Delta_{C}

\Delta_{D}

\Delta_{P}

, and MRPP; higher is better for W(1%).

Method	Budget	Inference (ms)
		SR	CA	PS
NeuroCore	3-call	29.6	65.9	37.2
NeuroCore	5-call	47.8	109.2	58.3
GQSAT	3-call	66.1	153.8	84.3
GQSAT	5-call	103.1	251.2	134.5
SATformer	one-shot	48.5	97.1	59.9

Appendix

Table 9: Neural inference cost of learning-based SAT branching methods. All values are average accumulated milliseconds per instance. Lower is better.

Dataset	Solver	NN Wait Ratio	NN Call Latency (s)
SC-2023	CaDiCaL (Native)	0.00%	–
SC-2023	CaDiCaL ( SAT-ACT )	11.99%	9.61
SC-2024	CaDiCaL (Native)	0.00%	–
SC-2024	CaDiCaL ( SAT-ACT )	5.79%	8.10
SC-2025	CaDiCaL (Native)	0.00%	–
SC-2025	CaDiCaL ( SAT-ACT )	7.92%	8.43

Appendix

Table 10: Neural-call overhead for the SAT Competition evaluation.

Boolean Satisfiability

See all 25 papers

Learning to Rank the Initial Branching Order of SAT Solvers
Mar 7, 2026Arvid Eriksson, Gabriel Poesia, Roman Bresson +2Boolean Satisfiability Constraint Satisfaction
KTH Royal Institute of Technology · Kempner Institute at Harvard University · Mohamed Bin Zayed University of Artificial Intelligence
Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving
Oct 17, 2026Haoze Wu, André Schidler, Armin Biere +1Boolean Satisfiability
Amherst College, Amherst, MA, USA · University of Freiburg, Freiburg im Breisgau, Germany · Broadcom, Palo Alto, CA, USA
Learning How to Cube
May 15, 2026Ferhat Erata, Sam Kouteili, Thanos Typaldos +4Transformer Constraint Satisfaction
Yale University · AWS Agentic AI

Mar 7, 2026J/K move · Enter open · S save

Learning to Rank the Initial Branching Order of SAT Solvers

Arvid Eriksson, Gabriel Poesia, Roman Bresson, Karl Henrik Johansson+1

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

Boolean Satisfiability Constraint Satisfaction Learning to Rank Graph Neural Networks

Open paper AskPDF arXiv

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.

Abstract

Boolean Satisfiability

Explore similar work

Learning to Rank the Initial Branching Order of SAT Solvers

Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

Learning How to Cube