March\_eq: Implementing additional reasoning into an efficient look-ahead SAT solver

DOI10.1007/11527695_26MaRDI QIDQ5714768zbMATH OpenOpenAlexFDO

Authors Marijn J. H. Heule, Mark Dufour, Joris van Zwieten, Hans van Maaren

Publication date 16 December 2005

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

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

Mathematics Subject Classification ID

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

Recommendations

• Present and Future of Practical SAT Solving
• March\_dl: adding adaptive heuristics and a new branching strategy
• Theory and Applications of Satisfiability Testing
• Effective Incorporation of Double Look-Ahead Procedures
• The quest for efficient Boolean satisfiability solvers

Cited in

(17)

• \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
• March_eq
• Equivalent literal propagation in the DLL procedure
• Logical cryptanalysis with WDSat
• Popularity-similarity random SAT formulas
• Exploiting the real power of unit propagation lookahead
• How to apply SAT-solving for the equivalence test of monotone normal forms
• Generating SAT instances with community structure
• March\_dl: adding adaptive heuristics and a new branching strategy
• On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
• Revisiting hyper binary resolution
• Automatic construction of parallel portfolios via algorithm configuration
• Present and Future of Practical SAT Solving
• Speedup techniques utilized in modern SAT solvers -- an analysis in the MIRA environment.
• SAT, gadgets, Max2XOR, and quantum annealers
• North-east lattice paths avoiding k collinear points via satisfiability
• The SAT-based approach to separation logic

This page was built for publication: March\_eq: Implementing additional reasoning into an efficient look-ahead SAT solver

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