Using machine learning classifiers in SAT branching

Bergin, Ruth Helen; Dalla, Marco; Visentin, Andrea; O'Sullivan, Barry; Provan, Gregory

Using machine learning classifiers in SAT branching

Files

SOCS2023___ML_for_SAT_Branching___AV.pdf(123.25 KB)

Accepted version

Date

2023-07-02

Authors

Bergin, Ruth Helen

Dalla, Marco

Visentin, Andrea

O'Sullivan, Barry

Provan, Gregory

Publisher

The AAAI Press

Published Version

https://doi.org/10.1609/socs.v16i1.27298

Abstract

The Boolean Satisfiability Problem (SAT) can be framed as a binary classification task. Recently, numerous machine and deep learning techniques have been successfully deployed to predict whether a CNF has a solution. However, these approaches do not provide a variables assignment when the instance is satisfiable and have not been used as part of SAT solvers. In this work, we investigate the possibility of using a machine-learning SAT/UNSAT classifier to assign a truth value to a variable. A heuristic solver can be created by iteratively assigning one variable to the value that leads to higher predicted satisfiability. We test our approach with and without probing features and compare it to a heuristic assignment based on the variable's purity. We consider as objective the maximisation of the number of literals fixed before making the CNF unsatisfiable. The preliminary results show that this iterative procedure can consistently fix variables without compromising the formula's satisfiability, finding a complete assignment in almost all test instances.

Keywords

Search in Boolean satisfiability , Machine and deep learning in search , Random vs systematic search strategy selection , Time , Memory , Solution quality trade-offs , Combinatorial Search , Artificial intelligence , Machine learning , Search strategy selection , Boolean satisfiability problem (SAT)

Citation

Bergin, R.H., Dalla, M., Visentin, A., O’Sullivan, B. and Provan, G. (2023) ‘Using machine learning classifiers in SAT branching’, Sixteenth International Symposium on Combinatorial Search, Proceedings of the International Symposium on Combinatorial Search, 16(1), pp. 169–170, https://doi.org/10.1609/socs.v16i1.27298