Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints

TL;DR

This paper presents a machine learning approach to automatically select the most effective SAT encodings for pseudo-Boolean and linear constraints, improving performance across various problem classes.

Contribution

It introduces a new feature set tailored for constraint problems and demonstrates effective encoding selection, outperforming existing methods like AutoFolio.

Findings

Effective encoding selection using a new feature set.

Good generalization to unseen problem classes.

Comparison showing superior performance over AutoFolio.

Abstract

Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudo-Boolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems; however we obtain better performance with a new set of features specifically designed for the pseudo-Boolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method.