2026-09-20T08:53:39Zhttps://cora.ucc.ie/server/oai/request

oai:cora.ucc.ie:10468/179332025-10-02T02:03:03Zcom_10468_388com_10468_5com_10468_227com_10468_2481com_10468_6com_10468_1col_10468_389col_10468_511col_10468_5231col_10468_8983

O'Sullivan, Barry Visentin, Andrea Dalla, Marco Research Ireland Centre for Research Training in Artificial Intelligence Insight SFI Research Centre for Data Analytics Science Foundation Ireland 2025-10-01T13:23:49Z 2025-10-01T13:23:49Z 2024 2024 The intersection of machine learning and propositional Boolean Satisfiability (SAT) offers transformative possibilities for solving some of the most challenging computational problems. This thesis investigates the use of modern machine learning (ML) and deep learning (DL) methodologies to enhance Boolean Satisfiability and Model Counting. Building upon the foundational understanding of SAT and its role as an NP-complete problem, this work addresses challenges related to structural reasoning, satisfiability and model counting prediction, feature extraction and instance generation. The contributions of this research are varied. First, by leveraging a diverse array of features and representations, we develop machine learning algorithms for SAT/UNSAT classification, problem categorization, and approximate model counting. These models demonstrate predictive accuracy and superior computational efficiency compared to traditional handcrafted heuristics. Second, we automate these procedures through the deployment of deep learning algorithms, significantly reducing dependency on manual engineering while improving adaptability to diverse SAT instances. Finally, we extend the application of the deep learning architectures to SAT instance generation. These approaches enable the generation of structurally diverse, statistically realistic SAT instances that serve as robust benchmarks for solver evaluation. The introduction of novel evaluation metrics ensures the practical utility of these generative models, emphasizing their contributions to advancing SAT-solving strategies. Through an extensive comparative analysis of traditional and machine learning driver SAT-analysis methodologies, this thesis extends the body of work that focuses on the integration of these paradigms. Its findings contribute to the broader field of computational logic, offering insights into scalable and interpretable solutions for Boolean reasoning tasks. Not peer reviewed Accepted Version application/pdf Dalla, M. 2024. Machine learning for structural reasoning in Boolean Satisfiability. PhD Thesis, University College Cork. 164 https://hdl.handle.net/10468/17933 en University College Cork info:eu-repo/grantAgreement/SFI/Research Centres Programme/16/RC/3918/IE/Confirm Centre for Smart Manufacturing/ info:eu-repo/grantAgreement/SFI/Research Centres Programme::Phase 2/12/RC/2289_P2/IE/INSIGHT_Phase 2 / info:eu-repo/grantAgreement/SFI/NSF Student Mobility Programme/18/CRT/6223 (S1)/IE/18/CRT/6223 Supplement/ © 2024, Marco Dalla. https://creativecommons.org/publicdomain/zero/1.0/ Boolean Satisfiability Machine learning Deep learning Instance generation Machine learning for structural reasoning in Boolean Satisfiability Doctoral thesis Doctoral PhD - Doctor of Philosophyinfo:eu-repo/semantics/openAccess