Conference item
Automatic generation of propagation complete SAT encodings
- Abstract:
-
Almost all applications of SAT solvers generate Boolean formulae from higher level expression graphs by encoding the semantics of each operation or relation into propositional logic. All non-trivial relations have many different possible encodings and the encoding used can have a major effect on the performance of the system. This paper gives an abstract satisfaction based formalisation of one aspect of encoding quality, the propagation strength, and shows that propagation complete SAT encodi...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Accepted manuscript, pdf, 439.7KB)
-
- Publisher copy:
- 10.1007/978-3-662-49122-5_26
Authors
Funding
European Research Council
More from this funder
Bibliographic Details
- Publisher:
- Springer, Berlin, Heidelberg Publisher's website
- Host title:
- VMCAI 2016: Verification, Model Checking, and Abstract Interpretation
- Series:
- Lecture Notes in Computer Science
- Journal:
- international Conference on Verification, Model Checking, and Abstract Interpretation 2016 Journal website
- Volume:
- 9583
- Pages:
- 536-556
- Publication date:
- 2015-12-25
- DOI:
- ISSN:
-
0302-9743
- ISBN:
- 9783662491218
Item Description
- Pubs id:
-
pubs:573519
- UUID:
-
uuid:a0288804-7811-4e1a-84f2-8972e6960040
- Local pid:
- pubs:573519
- Source identifiers:
-
573519
- Deposit date:
- 2015-11-16
Terms of use
- Copyright holder:
- Springer-Verlag Berlin Heidelberg
- Copyright date:
- 2015
- Notes:
- Copyright © 2016 Springer-Verlag Berlin Heidelberg. This is the accepted manuscript version of the article. The final version is available online from Springer at: [DOI if we have it]
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record