Evaluating CDCL variable scoring schemes

DOI10.1007/978-3-319-24318-4_29MaRDI QIDQ3453243zbMATH OpenOpenAlexFDO

Authors Armin Biere, Andreas Fröhlich

Publication date 20 November 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-24318-4_29

Mathematics Subject Classification ID

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

Recommendations

• Theory and Applications of Satisfiability Testing
• \textsf{SATGraf}: visualizing the evolution of SAT formula structure in solvers
• SAT solving with reference points
• Exploiting multivalued knowledge in variable selection heuristics for SAT solvers
• Hardware and Software, Verification and Testing

Cites work

• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• A machine program for theorem-proving
• Adaptive Restart Strategies for Conflict Driven SAT Solvers
• BerkMin: A fast and robust SAT-solver
• Graph-Based Algorithms for Boolean Function Manipulation
• Hardware and Software, Verification and Testing
• Impact of Community Structure on SAT Solver Performance
• Inprocessing rules
• Reusing the assignment trail in CDCL solvers
• Solving propositional satisfiability problems
• The community structure of SAT formulas
• The fractal dimension of SAT formulas
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(10)

• On CDCL-Based Proof Systems with the Ordered Decision Strategy
• Efficient all-UIP learned clause minimization
• On dedicated CDCL strategies for PB solvers
• Internal slackening scoring methods
• Preprocessing of propagation redundant clauses
• Preprocessing of propagation redundant clauses
• The External Interface for Extending WASP
• Searching for i-good lemmas to accelerate safety model checking
• Learning rate based branching heuristic for SAT solvers
• SAT solving with reference points

Describes a project that uses

Uses Software

• Lingeling
• Glucose
• PicoSAT
• BerkMin
• Chaff
• SATO
• Siege
• MiniSat
• HaifaSat

This page was built for publication: Evaluating CDCL variable scoring schemes

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