There are no CNF problems

Peter J. Stuckey

doi:10.1007/978-3-642-39071-5_3

There are no CNF problems

Peter J. Stuckey

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

9 Citations (Scopus)

Abstract

SAT technology has improved rapidly in recent years, to the point now where it can solve CNF problems of immense size. But solving CNF problems ignores one important fact: there are NO problems that are originally CNF. All the CNF that SAT solvers tackle is the result of modelling some real world problem, and mapping the high-level constraints and decisions modelling the problem into clauses on binary variables. But by throwing away the high level view of the problem SAT solving may have lost a lot of important insight into how the problem is best solved. In this talk I will hope to persuade you that by keeping the original high level model of the problem one can realise immense benefits in solving hard real world problems.

Original language	English
Title of host publication	Theory and Applications of Satisfiability Testing, SAT 2013 - 16th International Conference, Proceedings
Publisher	Springer
Pages	19-21
Number of pages	3
ISBN (Print)	9783642390708
DOIs	https://doi.org/10.1007/978-3-642-39071-5_3
Publication status	Published - 15 Jul 2013
Externally published	Yes
Event	International Conference on Theory and Applications of Satisfiability Testing 2013 - Helsinki, Finland Duration: 8 Jul 2013 → 12 Jul 2013 Conference number: 16th

Publication series

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

Conference

Conference	International Conference on Theory and Applications of Satisfiability Testing 2013
Abbreviated title	SAT 2013
Country/Territory	Finland
City	Helsinki
Period	8/07/13 → 12/07/13

Access to Document

10.1007/978-3-642-39071-5_3

Cite this

Stuckey, P. J. (2013). There are no CNF problems. In Theory and Applications of Satisfiability Testing, SAT 2013 - 16th International Conference, Proceedings (pp. 19-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7962 LNCS). Springer. https://doi.org/10.1007/978-3-642-39071-5_3

@inproceedings{0729453c248c482d94a529762a25532e,

title = "There are no CNF problems",

abstract = "SAT technology has improved rapidly in recent years, to the point now where it can solve CNF problems of immense size. But solving CNF problems ignores one important fact: there are NO problems that are originally CNF. All the CNF that SAT solvers tackle is the result of modelling some real world problem, and mapping the high-level constraints and decisions modelling the problem into clauses on binary variables. But by throwing away the high level view of the problem SAT solving may have lost a lot of important insight into how the problem is best solved. In this talk I will hope to persuade you that by keeping the original high level model of the problem one can realise immense benefits in solving hard real world problems.",

author = "Stuckey, \{Peter J.\}",

year = "2013",

month = jul,

day = "15",

doi = "10.1007/978-3-642-39071-5\_3",

language = "English",

isbn = "9783642390708",

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

publisher = "Springer",

pages = "19--21",

booktitle = "Theory and Applications of Satisfiability Testing, SAT 2013 - 16th International Conference, Proceedings",

address = "Switzerland",

note = "International Conference on Theory and Applications of Satisfiability Testing 2013, SAT 2013 ; Conference date: 08-07-2013 Through 12-07-2013",

}

Stuckey, PJ 2013, There are no CNF problems. in Theory and Applications of Satisfiability Testing, SAT 2013 - 16th International Conference, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7962 LNCS, Springer, pp. 19-21, International Conference on Theory and Applications of Satisfiability Testing 2013, Helsinki, Finland, 8/07/13. https://doi.org/10.1007/978-3-642-39071-5_3

There are no CNF problems. / Stuckey, Peter J.
Theory and Applications of Satisfiability Testing, SAT 2013 - 16th International Conference, Proceedings. Springer, 2013. p. 19-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7962 LNCS).

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

TY - GEN

T1 - There are no CNF problems

AU - Stuckey, Peter J.

N1 - Conference code: 16th

PY - 2013/7/15

Y1 - 2013/7/15

N2 - SAT technology has improved rapidly in recent years, to the point now where it can solve CNF problems of immense size. But solving CNF problems ignores one important fact: there are NO problems that are originally CNF. All the CNF that SAT solvers tackle is the result of modelling some real world problem, and mapping the high-level constraints and decisions modelling the problem into clauses on binary variables. But by throwing away the high level view of the problem SAT solving may have lost a lot of important insight into how the problem is best solved. In this talk I will hope to persuade you that by keeping the original high level model of the problem one can realise immense benefits in solving hard real world problems.

AB - SAT technology has improved rapidly in recent years, to the point now where it can solve CNF problems of immense size. But solving CNF problems ignores one important fact: there are NO problems that are originally CNF. All the CNF that SAT solvers tackle is the result of modelling some real world problem, and mapping the high-level constraints and decisions modelling the problem into clauses on binary variables. But by throwing away the high level view of the problem SAT solving may have lost a lot of important insight into how the problem is best solved. In this talk I will hope to persuade you that by keeping the original high level model of the problem one can realise immense benefits in solving hard real world problems.

UR - https://www.scopus.com/pages/publications/84879897098

U2 - 10.1007/978-3-642-39071-5_3

DO - 10.1007/978-3-642-39071-5_3

M3 - Conference Paper

AN - SCOPUS:84879897098

SN - 9783642390708

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

SP - 19

EP - 21

BT - Theory and Applications of Satisfiability Testing, SAT 2013 - 16th International Conference, Proceedings

PB - Springer

T2 - International Conference on Theory and Applications of Satisfiability Testing 2013

Y2 - 8 July 2013 through 12 July 2013

ER -

There are no CNF problems

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this