Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantifier Elimination Meets Treewidth

Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, Naijun Zhan

TL;DR

This work tackles the high worst-case complexity of quantifier elimination for real arithmetic, focusing on $FME$ for $LRA$ and $CAD$ for $NRA$. It introduces a dynamic-programming framework built on tree decompositions of the input formula's primal graph to exploit sparsity; the approach yields a theoretical improvement: when the treewidth is a constant, the worst-case complexity of $FME$ and $CAD$ goes from $doubly$ exponential to $single$ exponential in the number of eliminated variables. It extends to general QE procedures and provides a correctness argument. Preliminary experiments on sparse $LRA$ and $NRA$ benchmarks show gains over heuristic methods on instances with low treewidth, suggesting practical impact for sparse QE problems.

Abstract

In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependency graph of quantified formulas. Utilizing tools from parameterized algorithms, we investigate the role of treewidth, a parameter that measures the graph's tree-likeness, in the process of quantifier elimination. A novel dynamic programming framework, structured over a tree decomposition of the dependency graph, is developed for applying FME and CAD, and is also extensible to general quantifier elimination procedures. Crucially, we prove that when the treewidth is a constant, the framework achieves a significant exponential complexity improvement for both FME and CAD, reducing the worst-case complexity bound from doubly exponential to single exponential. Preliminary experiments on sparse linear real arithmetic (LRA) and nonlinear real arithmetic (NRA) benchmarks confirm that our algorithm outperforms the existing popular heuristic-based approaches on instances exhibiting low treewidth.

Quantifier Elimination Meets Treewidth

TL;DR

This work tackles the high worst-case complexity of quantifier elimination for real arithmetic, focusing on for and for . It introduces a dynamic-programming framework built on tree decompositions of the input formula's primal graph to exploit sparsity; the approach yields a theoretical improvement: when the treewidth is a constant, the worst-case complexity of and goes from exponential to exponential in the number of eliminated variables. It extends to general QE procedures and provides a correctness argument. Preliminary experiments on sparse and benchmarks show gains over heuristic methods on instances with low treewidth, suggesting practical impact for sparse QE problems.

Abstract

In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependency graph of quantified formulas. Utilizing tools from parameterized algorithms, we investigate the role of treewidth, a parameter that measures the graph's tree-likeness, in the process of quantifier elimination. A novel dynamic programming framework, structured over a tree decomposition of the dependency graph, is developed for applying FME and CAD, and is also extensible to general quantifier elimination procedures. Crucially, we prove that when the treewidth is a constant, the framework achieves a significant exponential complexity improvement for both FME and CAD, reducing the worst-case complexity bound from doubly exponential to single exponential. Preliminary experiments on sparse linear real arithmetic (LRA) and nonlinear real arithmetic (NRA) benchmarks confirm that our algorithm outperforms the existing popular heuristic-based approaches on instances exhibiting low treewidth.
Paper Structure (4 sections, 3 equations, 4 figures)

This paper contains 4 sections, 3 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. LRA, NRA, and Quantifier Elimination
  4. Treewidth and Tree Decomposition

Figures (4)

  • Figure 1: An LRA formula $\Phi$
  • Figure 2: The primal graph of $\Phi$
  • Figure 3: A tree decomposition of \ref{['fig:primal']}
  • Figure 4: The nice tree decomposition of \ref{['fig:td']}. Gray nodes correspond to the nodes in \ref{['fig:td']}