Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex

Valentin Promies, Jasper Nalbach, Erika Ábrahám, Paul Kobialka

TL;DR

FMplex introduces a novel, singly exponential variable-elimination and satisfiability-checking framework for conjunctions of linear real arithmetic constraints by applying case-splitting on bound extrema and restricted projections. Building on Fourier-Motzkin elimination, it eliminates redundancies and leverages a DFS-based search with global and local conflict analysis that parallels the simplex method, while accommodating strict constraints via a delta-trick. The paper provides formal guarantees, explores connections to simplex and virtual substitution, and presents an extensive experimental evaluation showing FMplex outperforms Fourier-Motzkin on conjunctive inputs and complements, rather than replaces, classical simplex-based SMT solving. These findings suggest FMplex as a practical, incremental SMT backend for $LRA$ that can be integrated with existing solvers to improve coverage of hard instances.

Abstract

In this paper we present a quantifier elimination method for conjunctions of linear real arithmetic constraints. Our algorithm is based on the Fourier-Motzkin variable elimination procedure, but by case splitting we are able to reduce the worst-case complexity from doubly to singly exponential. The adaption of the procedure for SMT solving has strong correspondence to the simplex algorithm, therefore we name it FMplex. Besides the theoretical foundations, we provide an experimental evaluation in the context of SMT solving. This is an extended version of the authors' work previously published at the fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023).

FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex

TL;DR

FMplex introduces a novel, singly exponential variable-elimination and satisfiability-checking framework for conjunctions of linear real arithmetic constraints by applying case-splitting on bound extrema and restricted projections. Building on Fourier-Motzkin elimination, it eliminates redundancies and leverages a DFS-based search with global and local conflict analysis that parallels the simplex method, while accommodating strict constraints via a delta-trick. The paper provides formal guarantees, explores connections to simplex and virtual substitution, and presents an extensive experimental evaluation showing FMplex outperforms Fourier-Motzkin on conjunctive inputs and complements, rather than replaces, classical simplex-based SMT solving. These findings suggest FMplex as a practical, incremental SMT backend for that can be integrated with existing solvers to improve coverage of hard instances.

Abstract

In this paper we present a quantifier elimination method for conjunctions of linear real arithmetic constraints. Our algorithm is based on the Fourier-Motzkin variable elimination procedure, but by case splitting we are able to reduce the worst-case complexity from doubly to singly exponential. The adaption of the procedure for SMT solving has strong correspondence to the simplex algorithm, therefore we name it FMplex. Besides the theoretical foundations, we provide an experimental evaluation in the context of SMT solving. This is an extended version of the authors' work previously published at the fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023).
Paper Structure (21 sections, 14 theorems, 21 equations, 6 figures, 1 table, 2 algorithms)

This paper contains 21 sections, 14 theorems, 21 equations, 6 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Matrices
  4. Linear Constraints
  5. Variable Assignments
  6. Fourier-Motzkin Variable Elimination
  7. FMplex as Variable Elimination Procedure
  8. FMplex as Satisfiability Checking Procedure
  9. Solutions
  10. Conflicts
  11. Avoiding Redundant Checks
  12. Backtracking of Local Conflicts
  13. Strict Constraints
  14. Relation to Other Methods
  15. Simplex Algorithm
  16. ...and 6 more sections

Key Result

Theorem 2.1

Let $\capitalisewords{a} \in \mathbb{Q}^{m \times n}$ and $\bm{b} \in \mathbb{Q}^{m\times 1}$. Then the system $\capitalisewords{a} \bm{x} \leq \bm{b}$ is satisfiable if and only if for all $\bm{f} \in \mathbb{Q}^{1\times m}$ with $\bm{f} \geq 0$ and $\bm{f} \capitalisewords{a} = \bm{0}$ it holds $\

Figures (6)

  • Figure 1: Fourier-Motzkin elimination steps from \ref{['example:redundancies']}.
  • Figure 2: The search tree corresponding to \ref{['example:fmplex-elim-procedure']}. The very first leaf (bottom left) is already satisfiable, meaning that the rest would not need to be computed.
  • Figure 3: Algorithm trace described in \ref{['example:nonbasis']}.
  • Figure 4: Algorithm trace described in \ref{['example:backtracking']}.
  • Figure 5: Algorithm trace described in \ref{['example:strict']}.
  • ...and 1 more figures

Theorems & Definitions (37)

  • Theorem 2.1: Farkas' Lemma farkas1902theorie
  • Theorem 2.2: Fundamental Theorem of Linear Programming, as in luenberger1984linear
  • Definition 2.3
  • Definition 2.4: Fourier-Motzkin Variable Elimination
  • Definition 2.5: Redundancy
  • Lemma 2.6: Redundancy by Construction
  • Example 2.7
  • Example 3.1
  • Definition 3.2: Restricted Projection
  • Lemma 3.3
  • ...and 27 more