Seminario Interdipartimentale di Algoritmica
 
 
 

Dipartimento di Informatica e Sistemistica - DIS
via Salaria 113, piano secondo
Aula C2

Abstract:
The solution of specific instances of Boolean satisfiability finds many applications in the design and formal verification of software and hardware systems. SAT solvers achieved impressive progress in the last 6 years, but many practical instances remain difficult. We observe that in some cases this difficulty is due to symmetry, which may cause exponential duplication of work during SAT solving.

We describe improved techniques for detecting symmetries in instances of Boolean satisfiability, which are in essense reductions to the computational graph automorphism problem. After symmetries are extracted in terms of group generators, we build symmetry-breaking predicates and conjoin them with the original CNF formula. This allows one to speed up SAT-solving with a variety of existing software tools via pre- and post-processing.