Towards a Theory of Good SAT Representations

Oliver Kullmann (Swansea University)

SAT solving has become an important tool to solve search problems for example
from the verification domain, combinatorics, or for cryptanalysis. An obvious problem is the translation into CNF (conjunctive normal form): how to get a good translation?

We try to initiate a theory of "good SAT representations", as a kind of
"knowledge representation for SAT solvers". Currently, we concentrate on
translations of general building blocks, which could be for example some types
of constraints (for example cardinality constraints) or components like the
S-box in cryptographic ciphers.

The first theory-tool available is the notion of "hardness" hd(F), which
measures in a certain sense how hard it is for a SAT solver to retrieve
information from the representation F of a boolean function f.

In my talk I want to present this notion of "hardness", how it fits into
the landscape of "representations", and how to generalise this approach.

http://www.cs.swan.ac.uk/~csoliver/