On Irrelevant Literals in Pseudo-Boolean Constraint Learning

TL;DR

This paper investigates the presence of irrelevant literals in pseudo-Boolean constraints derived via cutting planes, revealing their impact on solver efficiency and suggesting the need for improved detection methods despite computational challenges.

Contribution

It identifies the problem of irrelevant literals in PB constraints and discusses the computational difficulty of detecting them, highlighting implications for solver performance.

Findings

Irrelevant literals can weaken constraints and increase proof size.

Detecting irrelevant literals is NP-hard, making practical removal challenging.

Current PB solvers may need redesign to handle irrelevant literals effectively.

Abstract

Learning pseudo-Boolean (PB) constraints in PB solvers exploiting cutting planes based inference is not as well understood as clause learning in conflict-driven clause learning solvers. In this paper, we show that PB constraints derived using cutting planes may contain \emph{irrelevant literals}, i.e., literals whose assigned values (whatever they are) never change the truth value of the constraint. Such literals may lead to infer constraints that are weaker than they should be, impacting the size of the proof built by the solver, and thus also affecting its performance. This suggests that current implementations of PB solvers based on cutting planes should be reconsidered to prevent the generation of irrelevant literals. Indeed, detecting and removing irrelevant literals is too expensive in practice to be considered as an option (the associated problem is NP-hard.