Generic ILP versus specialized 0-1 ILP: an update

Optimized solvers for the Boolean Satisfiability (SAT) problem have many applications in areas such as hardware and software verification, FPGA routing, planning, etc. Further uses are complicated by the need to express “counting constraints” in conjunctive normal form (CNF). Expressing such constraints by pure CNF leads to more complex SAT instances. Alternatively, those constraints can be handled by Integer Linear Programming (ILP), but generic ILP solvers may ignore the Boolean nature of 0-1 variables. Therefore specialized 0-1 ILP solvers extend SAT solvers to handle these so-called “pseudo-Boolean” constraints. This work provides an update on the on-going competition between generic ILP techniques and specialized 0-1 ILP techniques. To make a fair comparison, we generalize recent ideas for fast SAT-solving to more general 0-1 ILP problems that may include counting constraints and optimization. Another aspect of our comparison is evaluation on 0-1 ILP benchmarks that origi...

• Type: Conference
• Year: 2002
• Where: ICCAD
• Authors: Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
• Keywords: 0-1 Ilp Solvers, 0-1 Ilp Techniques, General 0-1 Ilp, Hardware, ICCAD 2002