Zchaff2004: An efficient SAT solver

Yogesh S. Mahajan; Zhaohui Fu; Sharad Malik

doi:10.1007/11527695_27

Zchaff2004: An efficient SAT solver

Yogesh S. Mahajan, Zhaohui Fu, Sharad Malik

Research output: Contribution to journal › Conference article › peer-review

93 Scopus citations

Abstract

The Boolean Satisfiability Problem (SAT) is a well known NP-Complete problem. While its complexity remains a source of many interesting questions for theoretical computer scientists, the problem has found many practical applications in recent years. The emergence of efficient SAT solvers which can handle large structured SAT instances has enabled the use of SAT solvers in diverse domains such as electronic design automation and artificial intelligence. These applications continue to motivate the development of faster and more robust SAT solvers. In this paper, we describe the popular SAT solver zchaff with a focus on recent developments.

Original language	English (US)
Pages (from-to)	360-375
Number of pages	16
Journal	LECTURE NOTES IN COMPUTER SCIENCE
Volume	3542
DOIs	https://doi.org/10.1007/11527695_27
State	Published - 2005
Event	7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004 - Vancouver, BC, Canada Duration: May 10 2004 → May 13 2004

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/11527695_27

Cite this

@article{4a3899f3b8fb4b98b33cd2fadc8fd17d,

title = "Zchaff2004: An efficient SAT solver",

abstract = "The Boolean Satisfiability Problem (SAT) is a well known NP-Complete problem. While its complexity remains a source of many interesting questions for theoretical computer scientists, the problem has found many practical applications in recent years. The emergence of efficient SAT solvers which can handle large structured SAT instances has enabled the use of SAT solvers in diverse domains such as electronic design automation and artificial intelligence. These applications continue to motivate the development of faster and more robust SAT solvers. In this paper, we describe the popular SAT solver zchaff with a focus on recent developments.",

author = "Mahajan, {Yogesh S.} and Zhaohui Fu and Sharad Malik",

year = "2005",

doi = "10.1007/11527695_27",

language = "English (US)",

volume = "3542",

pages = "360--375",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer Verlag",

note = "7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004 ; Conference date: 10-05-2004 Through 13-05-2004",

}

TY - JOUR

T1 - Zchaff2004

T2 - 7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004

AU - Mahajan, Yogesh S.

AU - Fu, Zhaohui

AU - Malik, Sharad

PY - 2005

Y1 - 2005

N2 - The Boolean Satisfiability Problem (SAT) is a well known NP-Complete problem. While its complexity remains a source of many interesting questions for theoretical computer scientists, the problem has found many practical applications in recent years. The emergence of efficient SAT solvers which can handle large structured SAT instances has enabled the use of SAT solvers in diverse domains such as electronic design automation and artificial intelligence. These applications continue to motivate the development of faster and more robust SAT solvers. In this paper, we describe the popular SAT solver zchaff with a focus on recent developments.

AB - The Boolean Satisfiability Problem (SAT) is a well known NP-Complete problem. While its complexity remains a source of many interesting questions for theoretical computer scientists, the problem has found many practical applications in recent years. The emergence of efficient SAT solvers which can handle large structured SAT instances has enabled the use of SAT solvers in diverse domains such as electronic design automation and artificial intelligence. These applications continue to motivate the development of faster and more robust SAT solvers. In this paper, we describe the popular SAT solver zchaff with a focus on recent developments.

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

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

U2 - 10.1007/11527695_27

DO - 10.1007/11527695_27

M3 - Conference article

AN - SCOPUS:26444568158

SN - 0302-9743

VL - 3542

SP - 360

EP - 375

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

Y2 - 10 May 2004 through 13 May 2004

ER -

Zchaff2004: An efficient SAT solver

Abstract

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this