PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving

The 2025 PACE Challenge evaluated (among others) new approaches for finding a minimum hitting set (MHS), where given a set of sets $𝒮$ the goal is to find a minimum size set $H$ – the hitting set – that intersects with all given sets, i.e., $\mathrm{\varnothing }\ne H\cap S,\text{ for all }S\in 𝒮$. The decision version of the problem is one of the original 21 NP-complete problems identified by Karp [12]. We present the details to our approach that uses a combination of MaxSAT and mixed integer programming (MIP) to tackle the problem.

The use of a MaxSAT solver is motivated by the success of a MaxSAT approach for the directed feedback vertex set problem at the 2022 PACE challenge, which could be converted into an implicit hit set problem, where not all sets are known a priori [13, 14]. Further, MHS can be seen as a special case of MaxSAT, where variables occur in only one polarity. However, the MaxSAT solver solves only 94 of the 100 public competition instances within 30 minutes, which necessitates a complementary approach for the remaining instances.

MaxSAT solvers often use MIP solvers, either as a preprocessing step or to explicitly solve an (implicit) MHS posed by the MaxSAT solver [9, 16]. The use of a MIP solver before the actual MaxSAT algorithm is motivated by the observation that MIP solvers are often faster on small but hard instances [3], which matches the characteristics of the MHS instances not solved by our MaxSAT solver. While neither solver can solve all public competition instances, combined they are able to solve all 100 instances within 30 minutes.

Our approach first preprocesses (Section 3) the instance and then passes it to either the MIP solver or our MaxSAT solver (Section 4) depending on the number of distinct elements of the instance: any instance with fewer than 250 distinct elements ($|{\bigcup }_{S\in 𝒮}S|$) is passed on to the MIP solver.

The preprocessing and MaxSAT implementations are ours and will be described subsequently. As the MIP solver, we use SCIP¹¹1https://www.scipopt.org [4] (version 8.1.0). Another advantage of this approach – although not used in our implementation – is that SCIP as well as MaxSAT offer a mode where the optimality of the solution can be certified [2, 8].

We use two simple preprocessing rules whose correctness follow from propositional logic and are also mentioned in hitting set literature [6].

1. 1.

   Whenever there exist two distinct elements $u$ and $v$ such that $v$ occurs in every set that $u$ occurs in, we can remove $u$ from all sets, as there exists a minimum hitting set not using $u$. Further, replacing $u$ by $v$ in a minimum hitting set yields another minimum hiting set.

2. 2.

   Whenever there exist two distinct sets $S,S^{\prime }\in 𝒮$ such that $S\subset S^{\prime }$, we can remove $S^{\prime }$, as any hitting set that intersects $S$ also intersects $S^{\prime }$.

Results show that the first rule is crucial for good performance, as SCIP does not solve several instances without this preprocessing. The reduction is also necessary to accurately identify instances that should be tackled using a MIP solver. Our experiments suggest that the second rule is unnecessary, as MIP and MaxSAT solvers already efficiently deal with this type of redundancy.

Proving that no hitting set of a given size exists is hard for SAT solvers when limiting the hitting set size with a single cardinality constraint. The reason for this behavior is that this propositional encoding provides very little structure that is exploitable by the SAT solver to avoid iterating over all possible sets of this given maximum size. Indeed, we expect that pure SAT encodings of the problem are similar to pigeonhole encodings, which are known to require exponential runtime for most SAT solvers [10]. This is relevant as most exact MaxSAT algorithms use a SAT solver in their backend.

We implement the core-guided algorithm OLL [1, 15] using Cadical 2.1.3 [5] with hyperparameters manually adjusted to MHS. Core-guided approaches use cores to dissect the MaxSAT instance into smaller parts and then connect these cores to form meta-cores. (Meta-)cores are used to reformulate the original MaxSAT instance, which introduces structure to the propositional formula visible to the internal SAT solver. This structure makes it easier for the SAT solver to find a minimum hitting set and prove optimality. Which (meta-)cores are used for these reformulations determines the structure of the propositional formula and can have immense impact on the time required to solve the instance [17].

Upper bounds are one way that can help find good (meta-)cors for MHS. We initially run local search for five seconds to get an initial solution. We use our implementation of the NuWLS local search algorithm [7] for this purpose. This upper bound guides the search for (meta-)cores, can avoid a costly last call to the SAT solver, and is also used to warmstart the MIP solver whenever the MHS instances is small.

We use the MIP solver in our approach to solve small and complex instances. However, results from experiments running the MaxSAT solver repeatedly with different settings show that our solver can solve these instances. The problem is that the runtimes vary by orders of magnitude with several being within half an hour. Further analysis showed that this is mainly due to the structure introduced by the reformulations [17]. So far we were not able to establish a sufficiently good strategy for finding (meta-)cores that provides consistently good results, but see this as an interesting future challenge.