Lookahead saturation with restriction for SAT

Anbulagan; John Slaney

doi:10.1007/11564751_53

Lookahead saturation with restriction for SAT

Anbulagan^*, John Slaney

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

6 Citations (Scopus)

Abstract

We present; a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic in Satz, a high-performance SAT solver, showing empirically that it significantly improves the performance on an extensive range of benchmark problems that exhibit, hard structure.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages	727-731
Number of pages	5
DOIs	https://doi.org/10.1007/11564751_53
Publication status	Published - 2005
Event	11th International Conference on Principles and Practice of Constraint Programming - CP 2005 - Sitges, Spain Duration: 1 Oct 2005 → 5 Oct 2005

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3709 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Conference on Principles and Practice of Constraint Programming - CP 2005
Country/Territory	Spain
City	Sitges
Period	1/10/05 → 5/10/05

Access to Document

10.1007/11564751_53

Cite this

Anbulagan, & Slaney, J. (2005). Lookahead saturation with restriction for SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 727-731). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3709 LNCS). https://doi.org/10.1007/11564751_53

@inproceedings{a4eee8abf3fd4936b220753630b65135,

title = "Lookahead saturation with restriction for SAT",

abstract = "We present; a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic in Satz, a high-performance SAT solver, showing empirically that it significantly improves the performance on an extensive range of benchmark problems that exhibit, hard structure.",

author = "Anbulagan and John Slaney",

year = "2005",

doi = "10.1007/11564751_53",

language = "English",

isbn = "3540292381",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "727--731",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

note = "11th International Conference on Principles and Practice of Constraint Programming - CP 2005 ; Conference date: 01-10-2005 Through 05-10-2005",

}

Anbulagan & Slaney, J 2005, Lookahead saturation with restriction for SAT. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3709 LNCS, pp. 727-731, 11th International Conference on Principles and Practice of Constraint Programming - CP 2005, Sitges, Spain, 1/10/05. https://doi.org/10.1007/11564751_53

Lookahead saturation with restriction for SAT. / Anbulagan; Slaney, John.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2005. p. 727-731 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3709 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Lookahead saturation with restriction for SAT

AU - Anbulagan,

AU - Slaney, John

PY - 2005

Y1 - 2005

N2 - We present; a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic in Satz, a high-performance SAT solver, showing empirically that it significantly improves the performance on an extensive range of benchmark problems that exhibit, hard structure.

AB - We present; a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic in Satz, a high-performance SAT solver, showing empirically that it significantly improves the performance on an extensive range of benchmark problems that exhibit, hard structure.

UR - http://www.scopus.com/inward/record.url?scp=33646189654&partnerID=8YFLogxK

U2 - 10.1007/11564751_53

DO - 10.1007/11564751_53

M3 - Conference contribution

SN - 3540292381

SN - 9783540292388

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 727

EP - 731

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 11th International Conference on Principles and Practice of Constraint Programming - CP 2005

Y2 - 1 October 2005 through 5 October 2005

ER -

Anbulagan, Slaney J. Lookahead saturation with restriction for SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2005. p. 727-731. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11564751_53

Lookahead saturation with restriction for SAT

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this