The Conflict-Driven Clause Learning (CDCL) framework integrates multiple heuristic components to solve Boolean satisfiability (SAT) problems through synergistic cooperation. Understanding the characteristics of these components in the underlying architecture provides crucial insights for designing corresponding methods to enhance the performance of CDCL solvers. Although numerous studies from diverse perspectives have been conducted, there remains a need to develop efficient methods and algorithms to meet the requirements for enhancing the performance efficiency of SAT solving. In this paper, we introduced two fundamental innovations: deep restart, a strategic reset mechanism that clears variable activity states while preserving learned clauses and making phase randomization, and assignment coverage time (CoverT), a novel metric quantifying the minimum—conflict count required to assign all variables at least once during search exploration. The CoverT metric provided unique insight into the characteristics of the instance structure, allowing dynamic adaptation of branching heuristics in our proposed Deep Restart-Enhanced Conflict-Driven Clause Learning algorithm framework (DR-CDCL). Experimental validation in 2021–2023 SAT Competition benchmarks demonstrated statistically significant improvements:<UnorderedList Mark="Bullet"> <ItemContent> 14 additional solved instances for satisfiable cases (352 <InlineEquation ID="IEq1"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="44196_2025_798_Article_IEq1.gif" Format="GIF" Height="6" Rendition="HTML" Resolution="72" Type="Linedraw" Width="21" /> </InlineMediaObject> <EquationSource Format="TEX">$\rightarrow $</EquationSource> <EquationSource Format="MATHML"><math> <mo stretchy="false">→</mo> </math></EquationSource> </InlineEquation> 366, <InlineEquation ID="IEq2"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="44196_2025_798_Article_IEq2.gif" Format="GIF" Height="16" Rendition="HTML" Resolution="72" Type="Linedraw" Width="62" /> </InlineMediaObject> <EquationSource Format="TEX">$p<0.05$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi>p</mi> <mo><</mo> <mn>0.05</mn> </mrow> </math></EquationSource> </InlineEquation> via McNemar’s test). </ItemContent> <ItemContent> 7.3% reduction in average runtime for SAT instances under the 5000 s timeout threshold. </ItemContent> </UnorderedList> Notably, the performance trade-off analysis revealed that while deep restart enhances solution diversity for satisfiable instances, it introduced a 2.1% overhead on unsatisfiable proofs due to clause learning pattern disruption, a phenomenon requiring further investigation. This work advances solver architecture design by establishing formal connections between exploratory search patterns and instance structural complexity. The implemented solution prototype and benchmark data are publicly available to facilitate reproducibility.

Instance Assignment Coverage Feature for Operation Control of SAT Solver

期刊论文
出版模式：

开放获取
发表日期：

2025年3月31日

查看全文

Zhihui Li,
Shuwei Chen,
Guanfeng Wu,
Yang Xu

摘要

The Conflict-Driven Clause Learning (CDCL) framework integrates multiple heuristic components to solve Boolean satisfiability (SAT) problems through synergistic cooperation. Understanding the characteristics of these components in the underlying architecture provides crucial insights for designing corresponding methods to enhance the performance of CDCL solvers. Although numerous studies from diverse perspectives have been conducted, there remains a need to develop efficient methods and algorithms to meet the requirements for enhancing the performance efficiency of SAT solving. In this paper, we introduced two fundamental innovations: deep restart, a strategic reset mechanism that clears variable activity states while preserving learned clauses and making phase randomization, and assignment coverage time (CoverT), a novel metric quantifying the minimum—conflict count required to assign all variables at least once during search exploration. The CoverT metric provided unique insight into the characteristics of the instance structure, allowing dynamic adaptation of branching heuristics in our proposed Deep Restart-Enhanced Conflict-Driven Clause Learning algorithm framework (DR-CDCL). Experimental validation in 2021–2023 SAT Competition benchmarks demonstrated statistically significant improvements:

14 additional solved instances for satisfiable cases (352 $\rightarrow $ $\to$ 366, $p<0.05$ $p < 0.05$ via McNemar’s test).

7.3% reduction in average runtime for SAT instances under the 5000 s timeout threshold.

Notably, the performance trade-off analysis revealed that while deep restart enhances solution diversity for satisfiable instances, it introduced a 2.1% overhead on unsatisfiable proofs due to clause learning pattern disruption, a phenomenon requiring further investigation. This work advances solver architecture design by establishing formal connections between exploratory search patterns and instance structural complexity. The implemented solution prototype and benchmark data are publicly available to facilitate reproducibility.