ShatterPB: symmetry-breaking for pseudo-Boolean formulas

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.

• Type: Conference
• Year: 2004
• Where: ASPDAC
• Authors: Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
• Keywords: 0-1 Ilp, ASPDAC 2004, Fundamental Eda Problem, Many Important Tasks