March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver This paper discusses several techniques to make the look-ahead architecture for satisfiability (Sat) solvers more competitive. Our contribution consists of reduction of the computational costs to perform look-ahead and a cheap integration of both equivalence reasoning and local learning. Most proposed techniques are illustrated with experimental results of their implementation in our solver march_eq.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Giráldez-Cru, Jesús; Levy, Jordi: Generating SAT instances with community structure (2016)
- Balint, Adrian; Belov, Anton; Järvisalo, Matti; Sinz, Carsten: Overview and analysis of the SAT challenge 2012 solver competition (2015) ioport
- Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter: On the van der Waerden numbers $\mathrmw(2; 3, t)$ (2014)
- Hyvärinen, Antti E.J.; Junttila, Tommi; Niemelä, Ilkka: Partitioning SAT instances for distributed solving (2010)
- Laitinen, Tero; Junttila, Tommi; Niemelä, Ilkka: Extending clause learning DPLL with parity reasoning (2010)
- Sabharwal, Ashish: SymChaff: Exploiting symmetry in a structure-aware satisfiability solver (2009)
- Kullmann, Oliver: Present and future of practical SAT solving (2008)
- Herwig, P.R.; Heule, M.J.H.; van Lambalgen, P.M.; van Maaren, H.: A new method to construct lower bounds for van der Waerden numbers (2007)
- Haanpää, Harri; Järvisalo, Matti; Kaski, Petteri; Niemelä, Ilkka: Hard satisfiable clause sets for benchmarking equivalence reasoning techniques (2006)
- Armando, Alessandro; Castellini, Claudio; Giunchiglia, Enrico; Maratea, Marco: The SAT-based approach to separation logic (2005)
- Heule, Marijn; Dufour, Mark; van Zwieten, Joris; van Maaren, Hans: March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver (2005)