ShatterPB: symmetry-breaking for pseudo-Boolean formulas
F.A. Aloulb, Arathi Ramani, Igor L. Markov, Karem A. Sakallah · Asia and South Pacific Design Automation Conference · 2004
Many important tasks in circuit design and verification can be performed in practice via reductions to Boolean Satisfiability (SAT), making SAT a fundamental EDA problem. However such reductions often leave out application-specific structure, thus handicapping EDA tools in their competition with creative engineers. Successful attempts to represent and utilize additional structure on Boolean variables include recent work on 0--1 Integer Linear Programming (ILP) and on symmetries in SAT. Those extensions gracefully accommodate well-known advances in SAT-solving, but their combined use has not been attempted previously. Our work shows (i) how one can detect and use symmetries in instances of 0--1 ILP, and (ii) what benefits this may bring.