March-eq - Implementing additional reasoning into efficient look-ahead SAT solver

MJH Heule, M Dufour, JE van Zwieten, H van Maaren

Research output: Contribution to journalArticleScientificpeer-review


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.
Original languageUndefined/Unknown
Pages (from-to)345-359
Number of pages15
JournalLecture Notes in Computer Science
Publication statusPublished - 2005


  • academic journal papers
  • ZX CWTS JFIS < 1.00

Cite this