Automatic generation of propagation complete SAT encodings
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...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Published: |
Springer, Berlin, Heidelberg
2015
|