Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantifier Elimination for Normal Cone Computations

Michael Mandlmayr, Ali Kemal Uncu

TL;DR

This work addresses the challenge of computing regular normal cones for constraint sets when standard constraint qualifications fail, by formulating the problem in a semi-algebraic, quantifier-elimination framework. It develops a CAD-based, divide-and-conquer workflow to obtain exact descriptions of $\hat{N}_C(\bar{x})$, enabling efficient membership tests and the construction of co-derivatives for semismooth* Newton methods. The authors demonstrate an algorithmic pipeline that decomposes the constraint set into CAD cells, computes upper estimates of the normal cone on each cell, and refines them via SMT/QE, with a detailed Coulomb friction example as a proving ground. Overall, the approach provides a principled, automated alternative to gradient-based KKT methods, with potential as a preprocessing step for optimization and for automating co-derivative computations, albeit with the known complexity limitations of CAD.

Abstract

We present effective procedures to calculate regular normal cones and other related objects using quantifier elimination. This method of normal cone calculations is complementary to computing Lagrangians and it works best at points where the constraint qualifications fail and extra work for other methods becomes inevitable. This method also serves as a tool to calculate the regular co-derivative for semismooth* Newton methods. We list algorithms and their demonstrations of different use cases for this approach.

Quantifier Elimination for Normal Cone Computations

TL;DR

This work addresses the challenge of computing regular normal cones for constraint sets when standard constraint qualifications fail, by formulating the problem in a semi-algebraic, quantifier-elimination framework. It develops a CAD-based, divide-and-conquer workflow to obtain exact descriptions of , enabling efficient membership tests and the construction of co-derivatives for semismooth* Newton methods. The authors demonstrate an algorithmic pipeline that decomposes the constraint set into CAD cells, computes upper estimates of the normal cone on each cell, and refines them via SMT/QE, with a detailed Coulomb friction example as a proving ground. Overall, the approach provides a principled, automated alternative to gradient-based KKT methods, with potential as a preprocessing step for optimization and for automating co-derivative computations, albeit with the known complexity limitations of CAD.

Abstract

We present effective procedures to calculate regular normal cones and other related objects using quantifier elimination. This method of normal cone calculations is complementary to computing Lagrangians and it works best at points where the constraint qualifications fail and extra work for other methods becomes inevitable. This method also serves as a tool to calculate the regular co-derivative for semismooth* Newton methods. We list algorithms and their demonstrations of different use cases for this approach.
Paper Structure (10 sections, 3 theorems, 45 equations, 2 figures, 5 algorithms)

This paper contains 10 sections, 3 theorems, 45 equations, 2 figures, 5 algorithms.

Table of Contents

  1. Introduction
  2. Some Background on Optimization
  3. Constraint Optimization
  4. Semismooth* Newton methods
  5. Some Background on Quantifier Elimination
  6. A semi-algebraic description
  7. Main Results
  8. Other Applications to Semismooth* Newton Method
  9. outlook
  10. Acknowledgement

Key Result

Theorem 1

RockWets98 For a differentiable function $f:\mathbb{R}^n\to\mathbb{R}$ and a closed set $C\subset\mathbb{R}^n$ a necessary condition for $\bar{x}$ being locally optimal is which is equivalent to

Figures (2)

  • Figure 1: Example of KKT conditions failing to identify the entire regular normal cone calculated at $(0,0)$, the blue shaded region.
  • Figure 2: The graph of the regular normal cone mapping for $C:=[xy=0 \land x\geq 0\land y\geq 0].$

Theorems & Definitions (16)

  • Definition 1: Definition 6.3, pg 199, RockWets98
  • Definition 2
  • Definition 3
  • Theorem 1
  • Theorem 2
  • Definition 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Example 1
  • ...and 6 more