IndiCon: Selecting SAT Encodings for Individual Pseudo-Boolean and Linear Integer Constraints

TY - GEN

T1 - IndiCon: Selecting SAT Encodings for Individual Pseudo-Boolean and Linear Integer Constraints

AU - Ulrich-Oltean, Felix

AU - Nightingale, Peter

AU - Walker, James Alfred

N1 - Conference code: 36

PY - 2024/10/30

Y1 - 2024/10/30

N2 - Encoding to SAT and applying a state-of-the-art SAT solver can be a highly effective way of solving constraint problems. For many types of constraints there exist several alternative SAT encodings; and the choice of encoding can significantly affect SAT solver performance for any given problem. Previous work has shown that machine learning (ML) can be used to select SAT encodings for some constraint types, making a choice for each relevant constraint type in a problem instance. The state-of-the-art approach achieves good performance by first building a small portfolio of configurations, then selecting a configuration for a given problem instance using an ML model. The approach necessitates generating training data for every combination of encodings for the constraint types, thus it scales exponentially as more constraint types are added. In this work, we select potentially different encodings for each individual constraint in a problem instance. We are able to match the state-of-the-art performance while avoiding any limitation on the number of constraint types considered. To achieve this we are proposing new individual constraint features, we present a novel method for generating training data, and we have developed a new machine learning pipeline involving both unsupervised and supervised learning.

AB - Encoding to SAT and applying a state-of-the-art SAT solver can be a highly effective way of solving constraint problems. For many types of constraints there exist several alternative SAT encodings; and the choice of encoding can significantly affect SAT solver performance for any given problem. Previous work has shown that machine learning (ML) can be used to select SAT encodings for some constraint types, making a choice for each relevant constraint type in a problem instance. The state-of-the-art approach achieves good performance by first building a small portfolio of configurations, then selecting a configuration for a given problem instance using an ML model. The approach necessitates generating training data for every combination of encodings for the constraint types, thus it scales exponentially as more constraint types are added. In this work, we select potentially different encodings for each individual constraint in a problem instance. We are able to match the state-of-the-art performance while avoiding any limitation on the number of constraint types considered. To achieve this we are proposing new individual constraint features, we present a novel method for generating training data, and we have developed a new machine learning pipeline involving both unsupervised and supervised learning.

M3 - Conference contribution

BT - 2024 IEEE 36th International Conference on Tools with Artificial Intelligence

PB - IEEE Computer Society

T2 - IEEE International Conference on Tools with Artificial Intelligence

Y2 - 28 October 2024 through 30 October 2024

ER -