Dynamic symmetry-breaking for improved Boolean optimization

With impressive progress in Boolean Satisfiability (SAT) solving and several extensions to pseudo-Boolean (PB) constraints, many applications that use SAT, such as highperformance formal verification techniques are still restricted to checking satisfiability of certain conditions. However, there is also frequently a need to express a preference for certain solutions. Extending SAT-solving to Boolean optimization allows the use of objective functions to describe a desirable solution. Although recent work in 0-1 Integer Linear Programming (ILP) offers extensions that can optimize a linear objective function, this is often achieved by solving a series of SAT or ILP decision problems. Our work articulates some pitfalls of this approach. An objective function may complicate the use of any symmetry that might be present in the given constraints, even when the constraints are unsatisfiable and the objective function is irrelevant. We propose several new techniques that treat objective fu...

• Type: Conference
• Year: 2005
• Where: ASPDAC
• Authors: Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
• Keywords: ASPDAC 2005, Boolean Optimization, Linear Objective Function, Objective Function