Processing Online SAT Instances with Waiting Time Constraints and Completion Weights

摘要

In online scheduling, jobs arrive over time and information about future jobs is typically unknown. In this paper, we consider online scheduling problems where an unknown and independent set of Satisfiability (SAT) problem instances are released at different points in time for processing. We assume an existing problem where instances can remain unsolved and must start execution before a waiting time constraint is met. We also extend the problem by including instance weights and used an existing approach that combines the use of machine learning, interruption heuristics, and an extension of a Mixed Integer Programming (MIP) model to maximize the total weighted number of solved instances that satisfy the waiting time constraints. Experimental results over an extensive set of SAT instances show an improvement of up to 22.3 x with respect to generic ordering policies.