On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization

Unit propagation-based (UP) lower bounds are used in the vast majority of current Max-SAT solvers. However, lower bounds based on UP have seldom been applied in PseudoBoolean Optimization (PBO) algorithms derived from the DPLL procedure for Propositional Satisfiability (SAT). This paper enhances a DPLL-style PBO algorithm with an UP lower bound, and establishes conditions that enable constraint learning and non-chronological backtracking in the presence of conflicts involving constraints generated by the UP lower bound. From a theorical point of view, the paper highlights the relationship between the recent UP lower bound and the well-known Maximum Independent Set (MIS) lower bound. Finally, the paper provides preliminary results that show the effectiveness of the proposed approach for representative sets of instances.

• Type: Conference
• Year: 2008
• Where: FLAIRS
• Authors: Federico Heras, Vasco M. Manquinho, João Marques-Silva
• Keywords: Artificial Intelligence, Current Max-sat Solvers, DPLL-style PBO Algorithm, FLAIRS 2008, Lower Bound