Towards a Theory of Good SAT Representations

Oliver Kullmann (Swansea University)

May 11th, 14:00 in KE LT1


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.

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc
E: MSc

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom


AccessAble logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.