Narrow Results

The goal of this work is to study the portfolio problem which consists in finding a good combination of multiple heuristics given a set of a problem instances to solve. We are interested in a parallel context where the resources are assumed to be discrete and homogeneous, and where it is not possible to allocate a given resource (processor) to more than one heuristic. The objective is to minimize the average completion time over the whole set of instances. We extend in this paper some existing analysis on the problem. More precisely, we provide a new complexity result for the restricted version of the problem, then, we generalize previous approximation schemes. In particular, they are improved using a guess approximation technique. Experimental results are also provided using a benchmark of instances on SAT solvers.

This chapter presents the Horn-First Combinatorial Strategy (HFCS) within the Conflict-Driven Clause Learning (CDCL) solver framework, which leverages unit propagation to resolve conflicts via a directed acyclic entailment diagram. HFCS boosts the role of Horn clauses in clause management and their strategic use in solving, emphasizing learning clauses generated from their in-volvement. Experimental results confirm HFCS significantly enhances solver performance.