|
|
Symmetries in Boolean SAT
and 0-1 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 0-1 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 black-box SAT/ILP solvers by
adding a small number of new clauses (symmetry-breaking
predicates).
We describe
low-overhead reductions of symmetry-detection to the graph automorphism
problem and improve previously published
symmetry-breaking 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
previously-published quadratic constructions. These improvements are
validated empirically using recent
software for graph automorphism, SAT and 0-1 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.
|