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.

翻译：隐式命中集（IHS）方法为以声明方式解决计算困难的组合优化问题提供了一个通用框架。IHS在用于提取不一致性来源的决策预言机与用于计算累积不一致性来源上所谓命中集（HS）的优化器之间迭代运行。虽然决策预言机是语言特定的，但优化器通常通过整数规划进行实例化。我们探索了基于伪布尔（PB）推理不同应用方式以及随机局部搜索的命中集优化替代算法技术。我们广泛评估了这些替代方案的实际可行性，特别是在伪布尔（0-1整数规划）优化这一IHS最新实例化场景中。研究揭示了效率与可靠性之间的权衡：尽管商业整数规划求解器仍是实例化HS计算最有效的方式，但其可能因数值不稳定性导致正确性问题；事实上，我们证明通过PB推理实例化的精确HS计算可与数值精确的整数规划求解器竞争。此外，以PB推理作为HS计算基础，能够为IHS计算的正确性提供证明证书，该方法普遍适用于任何IHS实例化场景，只要所用声明式语言的推理过程可纳入我们采用的基于PB的证明格式。