Machine learning for structural reasoning in Boolean Satisfiability

Dalla, Marco

Machine learning for structural reasoning in Boolean Satisfiability

dc.contributor.advisor	O'Sullivan, Barry
dc.contributor.advisor	Visentin, Andrea
dc.contributor.author	Dalla, Marco	en
dc.contributor.funder	Research Ireland Centre for Research Training in Artificial Intelligence
dc.contributor.funder	Insight SFI Research Centre for Data Analytics
dc.contributor.funder	Science Foundation Ireland
dc.date.accessioned	2025-10-01T13:23:49Z
dc.date.available	2025-10-01T13:23:49Z
dc.date.issued	2024
dc.date.submitted	2024
dc.description.abstract	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.	en
dc.description.status	Not peer reviewed	en
dc.description.version	Accepted Version	en
dc.format.mimetype	application/pdf	en
dc.identifier.citation	Dalla, M. 2024. Machine learning for structural reasoning in Boolean Satisfiability. PhD Thesis, University College Cork.
dc.identifier.endpage	164
dc.identifier.uri	https://hdl.handle.net/10468/17933
dc.language.iso	en	en
dc.publisher	University College Cork	en
dc.relation.project	info:eu-repo/grantAgreement/SFI/Research Centres Programme/16/RC/3918/IE/Confirm Centre for Smart Manufacturing/
dc.relation.project	info:eu-repo/grantAgreement/SFI/Research Centres Programme::Phase 2/12/RC/2289_P2/IE/INSIGHT_Phase 2 /
dc.relation.project	info:eu-repo/grantAgreement/SFI/NSF Student Mobility Programme/18/CRT/6223 (S1)/IE/18/CRT/6223 Supplement/
dc.rights	© 2024, Marco Dalla.
dc.rights.uri	https://creativecommons.org/publicdomain/zero/1.0/
dc.subject	Boolean Satisfiability
dc.subject	Machine learning
dc.subject	Deep learning
dc.subject	Instance generation
dc.title	Machine learning for structural reasoning in Boolean Satisfiability
dc.type	Doctoral thesis	en
dc.type.qualificationlevel	Doctoral	en
dc.type.qualificationname	PhD - Doctor of Philosophy	en