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

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

doi:DOI:10.1007/11527695_26

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

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

Software Technology

Research output: Contribution to journal › Article › Scientific › peer-review

Abstract

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 language	Undefined/Unknown
Pages (from-to)	345-359
Number of pages	15
Journal	Lecture Notes in Computer Science
Volume	3542
DOIs	https://doi.org/DOI:10.1007/11527695_26
Publication status	Published - 2005

Keywords

academic journal papers
ZX CWTS JFIS < 1.00

Access to Document

DOI:10.1007/11527695_26

Cite this

@article{bf35316f3d514def9deac73848c4fc67,

title = "March-eq - Implementing additional reasoning into efficient look-ahead SAT solver",

abstract = "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 = "academic journal papers, ZX CWTS JFIS < 1.00",

author = "MJH Heule and M Dufour and {van Zwieten}, JE and {van Maaren}, H",

year = "2005",

doi = "DOI:10.1007/11527695_26",

language = "Undefined/Unknown",

volume = "3542",

pages = "345--359",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer",

}

TY - JOUR

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

AU - Heule, MJH

AU - Dufour, M

AU - van Zwieten, JE

AU - van Maaren, H

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

KW - academic journal papers

KW - ZX CWTS JFIS < 1.00

U2 - DOI:10.1007/11527695_26

DO - DOI:10.1007/11527695_26

M3 - Article

SN - 0302-9743

VL - 3542

SP - 345

EP - 359

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

ER -