ML Supported Predictions for SAT Solvers Performance

TL;DR

This paper develops a machine learning model that predicts the termination behavior of the CryptoMiniSat solver on hard SAT instances using early runtime parameters, enabling early estimation of solving success.

Contribution

It introduces a novel approach to classify SAT solver termination behavior early using runtime features, enhancing solver efficiency with AI integration.

Findings

Early runtime parameters can predict solver termination with high accuracy.

A feature vector based on initial iterations effectively classifies solver outcomes.

The approach offers a foundation for AI-enhanced SAT solvers.

Abstract

In order to classify the indeterministic termination behavior of the open source SAT solver CryptoMiniSat in multi-threading mode while processing hard to solve boolean satisfiability problem instances, internal solver runtime parameters have been collected and analyzed. A subset of these parameters has been selected and employed as features vector to successfully create a machine learning model for the binary classification of the solver's termination behavior with any single new solving run of a not yet solved instance. The model can be used for the early estimation of a solving attempt as belonging or not belonging to the class of candidates with good chances for a fast termination. In this context a combination of active profiles of runtime characteristics appear to mirror the influence of the solver's momentary heuristics on the immediate quality of the solver's resolution process. Because runtime parameters of already the first two solving iterations are enough to forecast termination of the attempt with good success scores, the results of the present work deliver a promising basis which can be further developed in order to enrich CryptoMiniSat or generally any modern SAT solver with AI abilities.