Presentation
NeuroSelect: Learning to Select Clauses in SAT Solvers
DescriptionModern SAT solvers depend on conflict-driven clause learning to avoid recurring conflicts. Deleting less valuable learned clauses is a crucial component of modern SAT solvers to ensure efficiency. However, a single clause deletion policy cannot guarantee optimal performance on all SAT instances. This paper introduces a new clause deletion metric to diversify existing clause deletion approaches. Then, we propose to use machine learning to evaluate and select clause deletion policies adaptively based on the input instance. We show that our method can reduce the runtime of the state-of-the-art SAT solver Kissat by 5.8\% on large industry benchmarks.
Event Type
Research Manuscript
TimeThursday, June 2710:45am - 11:00am PDT
Location3004, 3rd Floor
EDA
Design Verification and Validation