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.
Federico Heras, Vasco M. Manquinho, João Ma