Symmetry breaking for pseudo-Boolean formulas
Fadi Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah · ACM Journal of Experimental Algorithmics · 2008
Many important tasks in design automation and artificial intelligence can be performed in practice via reductions to Boolean satisfiability (SAT). However, such reductions often omit application-specific structure, thus handicapping 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 symmetries in SAT. Those extensions gracefully accommodate well-known advances in SAT solving, however, no previous work has attempted to combine both extensions. Our work shows (i) how one can detect and use symmetries in instances of 0-1 ILP, and (ii) what benefits this may bring.