

Symmetries in Boolean SAT
and 01 ILP
Prof.
Igor Markov
EECS
Dept., University
of Michigan
Friday, November 10th,
2003, 2pm  3pm
540A/B Cory Hall (D.O.P. Center Classroom)

Abstract
Instances of
Boolean satisfiability (SAT) and 01 Integer Linear Programming (ILP) arise in
formal verification, FPGA routing
and other applications. They often carry additional structure which allows one to
accelerate search. In this work we pursue (i) the detection of
symmetries, and (ii) using them to accelerate blackbox SAT/ILP solvers by
adding a small number of new clauses (symmetrybreaking
predicates).
We describe
lowoverhead reductions of symmetrydetection to the graph automorphism
problem and improve previously published
symmetrybreaking predicates (SBPs). In particular, we use the
cycle structure of symmetry generators, which typically involve very
few variables, to drastically reduce the size of SBPs.
Furthermore, our new SBPs grow linearly with the number of relevant
variables compared to
previouslypublished quadratic constructions. These improvements are
validated empirically using recent
software for graph automorphism, SAT and 01 ILP.
Speaker
Igor L.
Markov is an assistant professor of Electrical Engineering and Computer
Science at the University of Michigan. He did his master's (Math) and
doctorate (CS) work at UCLA.
Prof.
Markov's interests are in quantum computing and in combinatorial
optimization with applications to the design and verification of
integrated
circuits. Prof. Markov's contributions include the circuit placer Capo
and the quantum circuit simulator QuIDDPro.
