Automatic generation of propagation complete SAT encodings
| Autor: | Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Formalism (philosophy of mathematics)
Improved performance Theoretical computer science 010201 computation theory & mathematics Computer science 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0102 computer and information sciences 02 engineering and technology Propositional calculus 01 natural sciences Algorithm |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783662491218 VMCAI |
| Popis: | 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 encodings can be modelled by our formalism and automatically computed for key operations. This allows a more rigorous approach to designing encodings as well as improved performance. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|