Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach

Hannes Ihalainen, Dieter Vandesande, André Schidler, Jeremias Berg, Bart Bogaerts, Matti Järvisalo

TL;DR

This paper addresses the reliability and efficiency of solving hard combinatorial problems with the Implicit Hitting Set (IHS) approach. It investigates alternative hitting-set computations based on pseudo-Boolean (PB) reasoning and stochastic local search (SLS), pairing them with IP solvers and introducing certifiable proofs via VeriPB. The key contributions include a detailed general framework for solving HS components within IHS, multiple PB- and SLS-based instantiations (including SIS, CG, CB) and hybrid proof-producing configurations, and an extensive empirical evaluation demonstrating that certifiable PB-based HS can rival numerically exact IP solvers while offering correctness guarantees. The results show that combining IP solving, PB reasoning, and SLS yields robust performance with controllable proof overhead, enabling trustworthy IHS across PB and related declarative paradigms such as MaxSAT, CSPs, and abductive reasoning.

Abstract

The implicit hitting set (IHS) approach offers a general framework for solving computationally hard combinatorial optimization problems declaratively. IHS iterates between a decision oracle used for extracting sources of inconsistency and an optimizer for computing so-called hitting sets (HSs) over the accumulated sources of inconsistency. While the decision oracle is language-specific, the optimizers is usually instantiated through integer programming. We explore alternative algorithmic techniques for hitting set optimization based on different ways of employing pseudo-Boolean (PB) reasoning as well as stochastic local search. We extensively evaluate the practical feasibility of the alternatives in particular in the context of pseudo-Boolean (0-1 IP) optimization as one of the most recent instantiations of IHS. Highlighting a trade-off between efficiency and reliability, while a commercial IP solver turns out to remain the most effective way to instantiate HS computations, it can cause correctness issues due to numerical instability; in fact, we show that exact HS computations instantiated via PB reasoning can be made competitive with a numerically exact IP solver. Furthermore, the use of PB reasoning as a basis for HS computations allows for obtaining certificates for the correctness of IHS computations, generally applicable to any IHS instantiation in which reasoning in the declarative language at hand can be captured in the PB-based proof format we employ.

Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach

TL;DR

This paper addresses the reliability and efficiency of solving hard combinatorial problems with the Implicit Hitting Set (IHS) approach. It investigates alternative hitting-set computations based on pseudo-Boolean (PB) reasoning and stochastic local search (SLS), pairing them with IP solvers and introducing certifiable proofs via VeriPB. The key contributions include a detailed general framework for solving HS components within IHS, multiple PB- and SLS-based instantiations (including SIS, CG, CB) and hybrid proof-producing configurations, and an extensive empirical evaluation demonstrating that certifiable PB-based HS can rival numerically exact IP solvers while offering correctness guarantees. The results show that combining IP solving, PB reasoning, and SLS yields robust performance with controllable proof overhead, enabling trustworthy IHS across PB and related declarative paradigms such as MaxSAT, CSPs, and abductive reasoning.

Abstract

The implicit hitting set (IHS) approach offers a general framework for solving computationally hard combinatorial optimization problems declaratively. IHS iterates between a decision oracle used for extracting sources of inconsistency and an optimizer for computing so-called hitting sets (HSs) over the accumulated sources of inconsistency. While the decision oracle is language-specific, the optimizers is usually instantiated through integer programming. We explore alternative algorithmic techniques for hitting set optimization based on different ways of employing pseudo-Boolean (PB) reasoning as well as stochastic local search. We extensively evaluate the practical feasibility of the alternatives in particular in the context of pseudo-Boolean (0-1 IP) optimization as one of the most recent instantiations of IHS. Highlighting a trade-off between efficiency and reliability, while a commercial IP solver turns out to remain the most effective way to instantiate HS computations, it can cause correctness issues due to numerical instability; in fact, we show that exact HS computations instantiated via PB reasoning can be made competitive with a numerically exact IP solver. Furthermore, the use of PB reasoning as a basis for HS computations allows for obtaining certificates for the correctness of IHS computations, generally applicable to any IHS instantiation in which reasoning in the declarative language at hand can be captured in the PB-based proof format we employ.

Paper Structure

This paper contains 25 sections, 1 theorem, 5 equations, 1 figure, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Pseudo-Boolean Optimization
  4. The Implicit Hitting Set Approach
  5. A Remark on Terminology
  6. Alternatives Approaches to Hitting Set Computations
  7. A General View on Hitting Set Solving
  8. Optimize using an IP Solver.
  9. Optimize using Conflict-Driven PB Optimization.
  10. Integrating Stochastic Local Search
  11. VeriPB Proofs for PBO-IHS
  12. Constraint ID and Variable Management.
  13. Non-Reified Solution-Improving Constraints.
  14. Proofs and IP Instantiations of Solve-HS
  15. Verify optimal solution (OptLB).
  16. ...and 10 more sections

Key Result

Proposition 1

Let $(F\xspace, O)$ be a PBO instance, $\alpha_{\mathit{best}}$ an optimal solution to $(F\xspace, O)$, $\mathcal{K}$ a set of cores of $(F\xspace, O)$, and $\gamma$ an optimal solution to $(\mathcal{K}, O)$. Then $\gamma(O) \leq \alpha_{\mathit{best}}(O)$.

Figures (1)

  • Figure 1: Comparison of runtime with and without proof logging. Times are in seconds.

Theorems & Definitions (2)

  • Proposition 1: e.g., SBJ21Pseudo-BooleanOptimizationImplicitHittingSets
  • Example 2