Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Empirical Evaluation of the Implicit Hitting Set Approach for Weighted CSPs
SAT technology has proven to be surprisingly effective in a large variety of domains. However, for the Weighted CSP problem dedicated algorithms have always been superior. One approach not well-studied so far is the use …
Are Hitting Formulas Hard for Resolution?
Hitting formulas, introduced by Iwama, are an unusual class of propositional CNF formulas. Not only is their satisfiability decidable in polynomial time, but even their models can be counted in closed form. This stands i…
A New Perspective for Shuttlecock Hitting Event Detection
This article introduces a novel approach to shuttlecock hitting event detection. Instead of depending on generic methods, we capture the hitting action of players by reasoning over a sequence of images. To learn the feat…
Event DetectionHitting time for Markov decision process
We define the hitting time for a Markov decision process (MDP). We do not use the hitting time of the Markov process induced by the MDP because the induced chain may not have a stationary distribution. Even it has a stat…
Imitation LearningOn some dynamical features of the complete Moran model for neutral evolution in the presence of mutations
We present a version of the classical Moran model, in which mutations are taken into account; the possibility of mutations was introduced by Moran in his seminal paper, but it is more often overlooked in discussing the M…