Electronic Systems Design Seminar


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)


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.


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.

©2002-2018 U.C. Regents