Using machine learning classifiers in SAT branching

Thumbnail Image
Bergin, Ruth Helen
Dalla, Marco
Visentin, Andrea
O'Sullivan, Barry
Provan, Gregory
Journal Title
Journal ISSN
Volume Title
The AAAI Press
Research Projects
Organizational Units
Journal Issue
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.
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)
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,
© 2023, Association for the Advancement of ArtificialIntelligence (