Towards Learning Infinite SMT Models (Work in Progress)

TL;DR

The paper tackles solving quantified SMT problems with uninterpreted functions in $UFLIA$ by learning piecewise-linear infinite models to guide MBQI. It introduces a semantic, data-driven method to fit piecewise-linear functions to finite ground points and encode them as SMT terms via $ITE$ expressions. The approach includes greedy and smarter predicate-splitting algorithms and is implemented in the SMT solver cvc5, showing improved SAT outcomes on satisfiable instances without slowing UNSAT. It also presents a method to generate satisfiable fragments to stress-test MBQI. Overall, the work extends MBQI with scalable, semantic model learning for infinite-model reasoning and demonstrates practical gains in SMT solving.

Abstract

This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of linear arithmetic with uninterpreted functions (UFLIA). The constructed models are piecewise linear. Such models are useful for satisfiable problems but also provide an alternative driver for model-based quantifier instantiation (MBQI).

Figures (1)

• Figure 1: Four snapshots of the iterative process of finding an infinite model for a binary relation $R$, as described in Algorithm \ref{['alg:predSmarter']}. The relation $R$ is constrained by two assertions: $R(x,y) \Rightarrow x = y$ and $x = y \Rightarrow R(x, y)$. Yellow color signifies false and blue color signifies true. Dots in the center are points with boolean values assigned by the solver. Rectangles in the background depict the current relation assigned to $R$. The last figure shows the state in which the algorithm found the desired relation.

Theorems & Definitions (1)

• Example 2.1