A clause-based heuristic for SAT solvers

DOI10.1007/11499107_4MaRDI QIDQ5713744zbMATH OpenOpenAlexFDO

Authors Nachum Dershowitz, Ziyad Hanna, Alexander Nadel

Publication date 15 December 2005

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

Full work available at URL https://doi.org/10.1007/b137280

Mathematics Subject Classification ID

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

Recommendations

• BerkMin: A fast and robust SAT-solver
• Progress in Artificial Intelligence
• Hardware and Software, Verification and Testing
• \textsc{HaifaSat}: a SAT solver based on an abstraction/refinement model
• scientific article; zbMATH DE number 5605058

Cited in

(30)

• Centrality-based improvements to CDCL heuristics
• Coverage-based clause reduction heuristics for CDCL solvers
• Clause vivification by unit propagation in CDCL SAT solvers
• Exploiting multivalued knowledge in variable selection heuristics for SAT solvers
• Solving SAT problem by heuristic polarity decision-making algorithm
• BerkMin: A fast and robust SAT-solver
• Performance of clause selection heuristics for saturation-based theorem proving
• Writing declarative specifications for clauses
• Adaptive application of SAT solving techniques
• On freezing and reactivating learnt clauses
• Reducing chaos in SAT-like search: finding solutions close to a given one
• Generating Diverse Solutions in SAT
• \textsc{HaifaSat}: a SAT solver based on an abstraction/refinement model
• March\_dl: adding adaptive heuristics and a new branching strategy
• Evaluating CDCL variable scoring schemes
• scientific article; zbMATH DE number 6519724 (Why is no real title available?)
• A Decision-Making Procedure for Resolution-Based SAT-Solvers
• Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases
• scientific article; zbMATH DE number 6874827 (Why is no real title available?)
• Solving the CLSP by a Tabu Search Heuristic
• SAT solving with reference points
• Better Decision Heuristics in CDCL through Local Search and Target Phases
• Progress in Artificial Intelligence
• Variable and clause ordering in an FSA approach to propositional satisfiability
• Concurrent clause strengthening
• A bit-encoding phase selection strategy for satisfiability solvers
• Speedup techniques utilized in modern SAT solvers -- an analysis in the MIRA environment.
• CirCUs: A hybrid satisfiability solver
• Hardware and Software, Verification and Testing
• Heuristic-based backtracking relaxation for propositional satisfiability

Describes a project that uses

Uses Software

• zChaff
• MiniSat
• Chaff
• Siege
• BerkMin
• Zchaff2004

This page was built for publication: A clause-based heuristic for SAT solvers

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