On the hardness of (satisfiable) conjunctive normal forms

Photograph of Matthew Gwynne

Matthew Gwynne

(Swansea University)

A new measure h(F ) of “hardness” for formulas F in conjunctive normal form (i.e., clause-sets) is introduced. h(F) for unsatisfiable clause-sets has been studied extensively in [1,2]. However, now we treat satisfiable clause-sets F differently.

h(F) for satisfiable F as defined in [1,2] has a specific algorithmic viewpoint. It measures resources based on forced assignments and probing, progressing in a breadth-first manner. Now we consider boolean functions and their representations, and our new measure looks at ”complete” representations of the underlying boolean function of F.

We present the SAT representation hypothesis: The task of solving or refuting a SAT problem efficiently is captured by constructing a representation of the underlying boolean function which is of low hardness. For large boolean functions, the task becomes then to find good decompositions such that the component functions have low hardness. What it means to be a good decomposition is the next fundamental question.

We consider translations of the Advanced Encryption Standard (AES) and Data Encryption Standard (DES) as examples. We provide translations which have low hardness for all sub-functions in natural decompositions. The performance of SAT solvers on these instances is experimentally investigated.

[1] Oliver Kullmann. Investigating a general hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Technical Report TR99-041, Electronic Colloquium on Computational Complexity (ECCC), October 1999.
[2] Oliver Kullmann. Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Annals of Mathematics and Artificial Intelligence, 40(3-4):303–352, March 2004.

Thursday 5th May 2011, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science