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

Heras Federico, Vasco Manquinho, Joao Marques-Silva

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 Pseudo-Boolean 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.

Subjects: 15. Problem Solving; 15.2 Constraint Satisfaction

Submitted: Feb 25, 2008

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.