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

arXiv: https://arxiv.org/abs/2508.07015 · HTML: https://mlsanity.com/paper/2508.07015/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 43 references that are in the map.
- First posted on arXiv 9 Aug 2025.

## Builds on (most cited first, 7 of 7)

- [The SCIP Optimization Suite 9.0](https://mlsanity.com/paper/2402.17702/) (2024)
- [Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs](https://mlsanity.com/paper/2209.12185/) (2022)
- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)
- [Propositional Abduction with Implicit Hitting Sets](https://mlsanity.com/paper/1604.08229/) (2016)
- [Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended algorithms and examples)](https://mlsanity.com/paper/2303.11712/) (2023)
- [A Computational Status Update for Exact Rational Mixed Integer Programming](https://mlsanity.com/paper/2101.09141/) (2021)
- [Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability](https://mlsanity.com/paper/2501.17493/) (2025)

## Built on by (most cited first, 1 of 1)

- [Towards a Certifying Grounder](https://mlsanity.com/paper/2607.21199/) (2026)

## Abstract (arXiv)

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.