Satisfiability Modulo Theories for finite domains

Abstract

This thesis investigates strategies to improve and extend modern SMT solving procedures to effectively handle problems involving finite domains, whether they are explicitly defined or concealed within the problem's encoding. The research comprises both theoretical analyses and empirical evaluations. The central contributions are twofold:

First, a quantifier elimination strategy is developed. The research reveals that quantifiers significantly hinder solver efficiency when applied to finite domains, using Sudoku as an example. An algorithm is introduced to automatically detect ``effective finite domains'' in quantified Skolem formulas over integers, and eliminate quantifiers through exhaustive instantiation. A prototype implementation is made, showing this procedure improves solver performance and can be used even with solvers lacking quantifier support.

Second, the thesis explores the theory of uninterpreted functions with domain cardinality constraints. It establishes the NP-completeness of the satisfiability problem for a set of literals in this theory. SAT-based algorithms extending classical congruence closure are proposed, ensuring the efficiency of congruence closure for large or infinite domains while transitioning to SAT solvers for smaller domains. The proposed algorithms await implementation and validation within an SMT framework. Notably, addressing the loss of conflict set generation and equality deduction when SAT is employed remains an open challenge for future research.