|
Electronic
Systems Design Seminar
|
|
Symmetries in Boolean SAT and 0-1 ILP
|
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.