A Concurrency Problem with Exponential DPLL(T) Proofs

TL;DR

This paper demonstrates that certain concurrency problems inherently require exponentially many conflicts in DPLL(T) SMT solvers, establishing fundamental proof complexity limits through theoretical criteria and empirical validation.

Contribution

It introduces a general criterion for lower bounds on theory conflicts in DPLL(T) proofs and applies it to show exponential complexity in solving specific concurrency problems.

Findings

Exponential lower bounds on theory conflicts for certain problems

Both encodings exhibit the same exponential proof complexity

Experimental results confirm theoretical bounds across solvers

Abstract

Many satisfiability modulo theories solvers implement a variant of the DPLL(T ) framework which separates theory-specific reasoning from reasoning on the propositional abstraction of the formula. Such solvers conclude that a formula is unsatisfiable once they have learned enough theory conflicts to derive a propositional contradiction. However some problems, such as the diamonds problem, require learning exponentially many conflicts. We give a general criterion for establishing lower bounds on the number of theory conflicts in any DPLL(T ) proof for a given problem. We apply our criterion to two different state-of-the-art symbolic partial-order encodings of a simple, yet representative concurrency problem. Even though one of the encodings is asymptotically smaller than the other, we establish the same exponential lower bound proof complexity for both. Our experiments confirm this theoretical lower bound across multiple solvers and theory combinations.