Domain-specific heuristic augmentation of SAT solvers on prize-collecting job scheduling problem

Abstract

We study the prize-collecting job scheduling problem with one common and multiple secondary resources, where the target is to collect the biggest score possible by constructing a feasible schedule with given constraints of jobs and resources. Many scheduling configurations, where a single asset can be used by all jobs separately and a set of assets can be shared among the same jobs, may be transformed to the format of this problem. Two main tasks of the problem are job selection and job sequencing, which we solve by domain-specific heuristic augmentation of a maximum satisfiability (Max-SAT) solver. The heuristic is based on dual bound values generated by relaxed (lower-bound) and restricted (upper-bound) multi-valued decision diagrams. To convert the data in a format compatible for the solver, we encode it to conjunctive normal form (CNF), and then, we augment the solver by initially modifying the lower bound to be calculated based on a solution obtained by the heuristic approach. For testing we compare the approaches to each other and review different key performance indicators. Based on the experiments results, we observed an improvement in the performance of the solver when it was augmented with the lower bound solution from the heuristic.