Automatic Generation of Implied Clauses for SAT

Lyndon Drake; Alan M. Frisch; Toby Walsh

doi:10.1007/3-540-46135-3_78

Automatic Generation of Implied Clauses for SAT

Lyndon Drake, Alan M. Frisch, Toby Walsh

Computer Science

Research output: Contribution to conference › Paper › peer-review

Abstract

Propositional satisfiability (SAT) is the archetypal NP-complete problem [1]. A great deal of recent SAT research, particularly on the performance of SAT solvers, has been driven by structured instances, which are obtained by mapping other problem classes into SAT. It is possible to efficiently solve a wide range of problems by mapping them into SAT and solving the SAT representation of the problem.

Original language	Undefined/Unknown
Pages	783
DOIs	https://doi.org/10.1007/3-540-46135-3_78
Publication status	Published - 2002

Access to Document

10.1007/3-540-46135-3_78

http://link.springer.de/link/service/series/0558/bibs/2470/24700783.htm

Cite this

@conference{07122f0bf0a7422681020d840385772c,

title = "Automatic Generation of Implied Clauses for SAT",

abstract = "Propositional satisfiability (SAT) is the archetypal NP-complete problem [1]. A great deal of recent SAT research, particularly on the performance of SAT solvers, has been driven by structured instances, which are obtained by mapping other problem classes into SAT. It is possible to efficiently solve a wide range of problems by mapping them into SAT and solving the SAT representation of the problem. ",

author = "Lyndon Drake and Frisch, {Alan M.} and Toby Walsh",

year = "2002",

doi = "10.1007/3-540-46135-3_78",

language = "Undefined/Unknown",

pages = "783",

}

TY - CONF

T1 - Automatic Generation of Implied Clauses for SAT

AU - Drake, Lyndon

AU - Frisch, Alan M.

AU - Walsh, Toby

PY - 2002

Y1 - 2002

N2 - Propositional satisfiability (SAT) is the archetypal NP-complete problem [1]. A great deal of recent SAT research, particularly on the performance of SAT solvers, has been driven by structured instances, which are obtained by mapping other problem classes into SAT. It is possible to efficiently solve a wide range of problems by mapping them into SAT and solving the SAT representation of the problem.

AB - Propositional satisfiability (SAT) is the archetypal NP-complete problem [1]. A great deal of recent SAT research, particularly on the performance of SAT solvers, has been driven by structured instances, which are obtained by mapping other problem classes into SAT. It is possible to efficiently solve a wide range of problems by mapping them into SAT and solving the SAT representation of the problem.

U2 - 10.1007/3-540-46135-3_78

DO - 10.1007/3-540-46135-3_78

M3 - Paper

SP - 783

ER -