On the proof complexity of MCSAT

TL;DR

This paper establishes a proof complexity equivalence between the MCSAT approach for SMT solving and the Res*(T) proof system, bridging the gap between practical solver efficiency and theoretical complexity bounds.

Contribution

It extends proof complexity analysis to MCSAT, showing its polynomial equivalence to Res*(T), and links CDCL(T) and MCSAT in proof-theoretic terms.

Findings

MCSAT is polynomially equivalent to Res*(T)

CDCL(T) and MCSAT are proof-theoretically equivalent

Provides a foundation for analyzing MCSAT's performance on formulas

Abstract

Satisfiability Modulo Theories (SMT) and SAT solvers are critical components in many formal software tools, primarily due to the fact that they are able to easily solve logical problem instances with millions of variables and clauses. This efficiency of solvers is in surprising contrast to the traditional complexity theory position that the problems that these solvers address are believed to be hard in the worst case. In an attempt to resolve this apparent discrepancy between theory and practice, theorists have proposed the study of these solvers as proof systems that would enable establishing appropriate lower and upper bounds on their complexity. For example, in recent years it has been shown that (idealized models of) SAT solvers are polynomially equivalent to the general resolution proof system for propositional logic, and SMT solvers that use the CDCL(T) architecture are polynomially equivalent to the Res*(T) proof system. In this paper, we extend this program to the MCSAT approach for SMT solving by showing that the MCSAT architecture is polynomially equivalent to the Res*(T) proof system. Thus, we establish an equivalence between CDCL(T) and MCSAT from a proof-complexity theoretic point of view. This is a first and essential step towards a richer theory that may help (parametrically) characterize the kinds of formulas for which MCSAT-based SMT solvers can perform well.