Machine learning for structural reasoning in Boolean Satisfiability

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.

Grantor dc:publisher

University College Cork

Year dc:date.issued

2024

Author dc:creator

• Dalla, Marco

Advisors dc:contributor.advisor

• O'Sullivan, Barry
• Visentin, Andrea

• Boolean Satisfiability
• Machine learning
• Deep learning
• Instance generation

Statement dc:rights

• © 2024, Marco Dalla.

Licence dc:rights.uri

• https://creativecommons.org/publicdomain/zero/1.0/

Language dc:language.iso

en

Handle dc:identifier.uri

https://hdl.handle.net/10468/17933

OAI identifier oai:identifier

oai:cora.ucc.ie:10468/17933