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.

References in zbMATH (referenced in 12 articles , 1 standard article )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Lindauer, Marius; Hoos, Holger; Leyton-Brown, Kevin; Schaub, Torsten: Automatic construction of parallel portfolios via algorithm configuration (2017)
  2. Giráldez-Cru, Jesús; Levy, Jordi: Generating SAT instances with community structure (2016)
  3. Balint, Adrian; Belov, Anton; Järvisalo, Matti; Sinz, Carsten: Overview and analysis of the SAT challenge 2012 solver competition (2015) ioport
  4. Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter: On the van der Waerden numbers $\mathrmw(2; 3, t)$ (2014)
  5. Hyvärinen, Antti E.J.; Junttila, Tommi; Niemelä, Ilkka: Partitioning SAT instances for distributed solving (2010)
  6. Laitinen, Tero; Junttila, Tommi; Niemelä, Ilkka: Extending clause learning DPLL with parity reasoning (2010)
  7. Sabharwal, Ashish: SymChaff: Exploiting symmetry in a structure-aware satisfiability solver (2009)
  8. Kullmann, Oliver: Present and future of practical SAT solving (2008)
  9. 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)
  10. Haanpää, Harri; Järvisalo, Matti; Kaski, Petteri; Niemelä, Ilkka: Hard satisfiable clause sets for benchmarking equivalence reasoning techniques (2006)
  11. Armando, Alessandro; Castellini, Claudio; Giunchiglia, Enrico; Maratea, Marco: The SAT-based approach to separation logic (2005)
  12. Heule, Marijn; Dufour, Mark; van Zwieten, Joris; van Maaren, Hans: March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver (2005)