Reusing the assignment trail in CDCL solvers

MaRDI QIDQ2786914zbMATH OpenFDO

Authors Peter van der Tak, Antonio Ramos, Marijn J. H. Heule

Publication date 23 February 2016

Published in Journal of Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)

zbMATH Keywords

CDCL solverrestart strategy

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Local Restarts
• Between restarts and backjumps
• Off the Trail: Re-examining the CDCL Algorithm
• Machine learning-based restart policy for CDCL SAT solvers
• A dynamic restart strategy for solving SAT problem

Cited in

(15)

• Machine learning-based restart policy for CDCL SAT solvers
• Coverage-based clause reduction heuristics for CDCL solvers
• The \textsc{MergeSat} solver
• Trade-offs between time and memory in a tighter model of CDCL SAT solvers
• Off the Trail: Re-examining the CDCL Algorithm
• Between restarts and backjumps
• Between SAT and UNSAT: the fundamental difference in CDCL SAT
• Evaluating CDCL variable scoring schemes
• Adaptive Restart Strategies for Conflict Driven SAT Solvers
• Local Restarts
• Assignment stack shrinking
• Recording and minimizing nogoods from restarts
• A dynamic restart strategy for solving SAT problem
• On enumerating short projected models
• Satisfiability modulo user propagators

This page was built for publication: Reusing the assignment trail in CDCL solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2786914)