Off-line and on-line scheduling of SAT instances with time processing constraints

Abstract

Many combinatorial problems (e.g., SAT) are well-known NP-complete problems. Therefore, many instances cannot be solved within a reasonable time, and the runtime varies from few seconds to hours or more depending on the instance. Cloud computing offers an interesting opportunity to solve combinatorial problems in different domains. Computational time can be rented by the hour and for a given number of processors, therefore it is extremely important to find a good balance between the number of solved instances and the requested resources in the cloud. In this work, we present two computational approaches (i.e., Off-line and On-line) that combine the use of machine learning and mixed integer programming in order to maximize the number of solved SAT instances. In the Off-line model, we assume to have all the instances before the processing phase begins. This approach attempts to maximize solved instances within a global time limit constraint. On the other hand, in the On-line model, instances with a maximum waiting time constraint have to be handled as they arrive. Thus, deciding which/when instances should be attended has a big impact in the amount of solved instances. Experimental validations with sets of SAT instances, suggest that our Off-line approach can solve up to 93% of the solvable instances within 50% of the overall execution time. Additionally, our On-line approach can solve up to 3.5x more instances than ordering policies such as FCFS and SJF.