Program Synthesis for Polynomial System using Algebraic Geometry

A polynomial $h\in\mathbb{R}[x_{1},\dots,x_{n}]$ is a sum of squares (SOS) iff there exist $k\geq 1$ and polynomials $g_{1},\dots,g_{k}\in\mathbb{R}[x_{1},\dots,x_{n}]$ such that $h=\sum_{i=1}^{k}g_{i}^{2}.$

Given a set $X\subseteq\mathbb{R}^{n}$ and a polynomial $g\in\mathbb{R}[x_{1},\dots,x_{n}]$, we say that $g$ is strongly positive over X if $\inf_{x\in X}g(x)>0$. We write this as $X\models g\gg 0.$

Let $\Phi=\{g_{1}\bowtie_{1}0,\dots,g_{k}\bowtie_{k}0\}$ be a set of polynomial inequalities where $\bowtie_{i}\in\{\geq,>\}$ and $g_{i}\in\mathbb{R}[x_{1},\dots,x_{n}]$. We define $\textsl{SAT}(\Phi)$ as the set of all real valuations $\val$ over the variables $\{x_{1},\dots,x_{n}\}$ that satisfy $\Phi.$ More formally, $\textsl{SAT}(\Phi)=\{\val\in\mathbb{R}^{n}~{}|~{}\bigwedge_{i=1}^{k}\val\models(g_{i}\bowtie_{i}0)\}.$

Given a set $X\subseteq\mathbb{R}^{n}$, we define $\overline{X}$ to be the closure of $X$ with respect to the Euclidean topology of $\mathbb{R}^{n}$. For a set $\Phi$ of polynomial inequalities, we define $\overline{\Phi}$ as the system of polynomial inequalities obtained from $\Phi$ by replacing every strict ineqaulity with its non-strict counterpart.

We are now ready to present the main mathematical theorems that will be used in our work. Our presentation follows that of [goharshady2020parameterized, Section 2.6], which also contains proofs of corollaries that are not proven here.

The importance of Farkas’ Lemma for us is that if we have a standard constraint of form (LABEL:eq:entailment-form) and if the constraint includes only linear/affine inequalities, then we can use this lemma in Step 3 of our algorithm to reduce the standard constraint to QP, just as we did in Section LABEL:sec:algo:overview. Moreover, Farkas’ Lemma guarantees that this approach is not only sound but also complete. A corner case that we have to consider is when $\Phi$ is itself unsatisfiable and thus $\Phi\Rightarrow\psi$ holds vacuously. Fortunately, Farkas’ Lemma also provides a criterion for unsatisfiability. In practice, we work with the following corollary of Theorem 4.2 which can also handle strict inequalities.

We now consider extensions of Farkas’ Lemma which can help us handle non-linear standard constraints in Step 3. The first extension is Handelman’s theorem, which can be applied when the inequalities on the left hand side of (LABEL:eq:entailment-form) are linear/affine, but the right hand side is a polynomial of arbitrary degree. To present the theorem, we first need the concept of monoids.

Consider a set $V=\{x_{1},\dots x_{r}\}$ of real-valued variables and the following system of linear inequalities over $V$:

where $\bowtie_{i}\in\{>,\geq\}$ for all $1\leq i\leq m$. Let $g_{i}$ be the left hand side of the $i$-th inequality, i.e. $g_{i}(x_{1},\dots,x_{r}):=a_{i,0}+a_{i,1}\cdot x_{1}+\dots a_{i,r}\cdot x_{r}$. The monoid of $\Phi$ is defined as:

In other words, the monoid contains all polynomials that can be obtained as a multiplication of the $g_{i}$’s. Note that $1\in\textsl{Monoid}(\Phi).$ We define $\textsl{Monoid}_{d}(\Phi)$ as the subset of polynomials in $\textsl{Monoid}(\Phi)$ of degree at most $d.$

The intuition here is that if every inequality in $\Phi$ holds, then all the LHS expressions in $\Phi$ are non-negative and hence any multiplication $h_{i}$ of them is also non-negative. As in the case of Farkas’ Lemma, Handelman’s theorem shows that this approach is not only sound but also complete. We also need a variant that can handle strict inequalities in $\Phi.$

Corollary 2 above can handle a wider family of standard constraints than Corollary 1. However, it is also more expensive, since we now need to generate one new variable $y_{i}$ for every polynomial in $\textsl{Monoid}_{d}(\Phi)$ instead of $\Phi$ itself. Moreover, there is no bound $d$ in the theorem itself, so introducing $d$ would lead to semi-completeness instead of completeness, i.e. the approach would be complete only if a large enough value of $d$ is used. As such, in cases where both sides of (LABEL:eq:entailment-form) are linear, Corollary 1 is preferable. We now consider a more expressive theorem that can handle polynomials on boths sides of (LABEL:eq:entailment-form).

As in the cases of Farkas and Handelman, we need a variant of of Theorem 4.4 that can handle strict inequalities in $\Phi.$

Trying to use the corollary above for handling standard constraints of form (LABEL:eq:entailment-form) in Step 3 of our algorithm leads to two problems: (i) we also need a criterion for unsatisfiability of $\Phi$ to handle the cases where $\Phi\Rightarrow\psi$ holds vacuously, and (ii) in our QP, we should somehow express the property that every $h_{i}$ is a sum of squares. We now show how each of these challenges can be handled. To handle (i), we need another classical theorem from real algebraic geometry.

We now combine the Real Nullstellensatz with Putinar’s Postivstellensatz to obtain a criterion for unsatisfiability of $\Phi.$

Finally, we provide the needed theorems to check that a certain polynomial $h$ is a sum of squares using QP.

Based on Theorems 4.7 and 4.8, a polynomial $p$ of degree $2\cdot d$ is a sum of squares if and only if it can be written as $p=a^{T}\cdot L\cdot L^{T}\cdot a$ such that diagonal entries of $L$ are non-negative. This representation provides us with a simple approach to generate a sum-of-squares polynomial of degree $2\cdot d$ with symbolic coefficients and encoding them in QP. We first generate a lower triangular matrix $L$ of order $\binom{n+d}{d}$ by creating one fresh variable for each entry in the lower triangle and adding the extra condition that the entries on the diagonal must be non-negative. Then, we symbolically compute $a^{T}\cdot L\cdot L^{T}\cdot a.$

Recall that at the end of Step 2, we have a finite set of standard constraints of form (LABEL:eq:entailment-form). In this step, the algorithm handles each standard constraint separately and reduces it to quadratic programming over template variables and newly-introduced variables, hence effectively eliminating the program variables and the quantification over them. Let $f_{1}\bowtie_{1}0~{}\wedge~{}f_{2}\bowtie_{2}0~{}\wedge~{}\ldots\wedge f_{r}\bowtie_{r}0\Rightarrow f\bowtie 0$ be one of the standard constraints. The algorithm considers three cases: (i) if all the inequalities on both sides of the constraint are affine, then it applies Farkas’ Lemma; (ii) if the LHS inequalities are affine but the RHS is a higher-degree polynomial, then the algorithm applies Handelman’s theorem; and (iii) if the LHS contains higher-degree polynomials, the algorithm applies the Stellensätze and Theorem 4.6. Below, we define $\Phi:\{f_{1}\bowtie_{1}0,f_{2}\bowtie_{2}0,\ldots,f_{r}\bowtie_{r}0\}$ and $\psi:f\bowtie 0.$

Assuming all the constraints in $\Phi$ and $\psi$ are affine, we can apply Corollary 1. Based on this corollary, we have to consider three cases disjunctively: {compactenum}

$\Phi$ is satisfiable and entails $\psi$: The algorithm creates new template variables $y_{0},\dots,y_{r}$ with the constraint $y_{i}\geq 0$ for every $i$. It then symbolically computes $f=y_{0}+\sum_{i=1}^{r}y_{i}\cdot f_{i}.$ The latter is a polynomial equality over $\vars.$ So, the algorithm equates the coefficients of corresponding monomials on both sides, hence reducing this case to QP. Additionally, if $\psi$ is a strict inequality, the algorithm adds the extra constraint $\sum_{\bowtie_{i}\in\{>\}}y_{i}>0.$

$\Phi$ is unsatisfiable and $-1\geq 0$ can be obtained: This is similar to the previous case, except that $-1$ should be written as $y_{0}+\sum_{i=1}^{r}y_{i}\cdot f_{i}.$

$\Phi$ is unsatisfiable and $0>0$ can be obtained: This is also similar to the last two cases. We have $0=y_{0}+\sum_{i=1}^{r}y_{i}\cdot f_{i}$ and $\sum_{\bowtie_{i}\in\{>\}}y_{i}>0.$ Note that the template variables $y$ are freshly generated in each case above. Also, we have to consider cases (2) and (3) because $\Phi$ is unsatisfiable in these cases and hence the constraint $\Phi\Rightarrow\psi$ always holds vacuously.

Assuming all constraints in $\Phi$ are linear but $\psi$ is a higher-degree polynomial inequality, the algorithm applies Corollaries 1 and 2. Again, we have to consider the same three cases as in Step 3.(i): {compactenum}

$\Phi$ is satisfiable and entails $\psi$: We apply Corollary 2. The algorithm first symbolically computes $\textsl{Monoid}_{d}(\Phi)=\{h_{1},h_{2},\dots,h_{u}\}.$ It then generates new template variables $y_{0},y_{1},\dots,y_{u}$ and constrains them by setting $y_{0},y_{1},y_{2},\dots,y_{u}\geq 0.$ If $\psi$ is a strict inequality, it further adds the constraint $y_{0}>0.$ It then symbolically computes the equality

As usual, this is an equality whose both sides are polynomials over $\vars.$ So, the algorithm equates the coefficients of corresponding monomials on the LHS and RHS, which reduces this case to QP.

Note that $\Phi$ consists of linear inequalities, so we can use Farkas’ Lemma to check if $\Phi$ is unsatisfiable. As such, this step is the same as case (2) of Step 3.(i).

This is the same as case (3) of Step 3.(i).

If $\Phi$ includes polynomial inequalities of degree $2$ or larger, then we have to apply Corollary 3 and Theorem 4.6. The algorithm considers three cases and combines them disjunctively: {compactenum}

$\Phi$ is satisfiable and entails $\psi$: In this case, we apply Corollary 3. The algorithm generates template sum-of-squares polynomials $h_{0},\ldots,h_{r}$ of degree $d$ and adds QP constraints that ensure each $h_{i}$ is a sum of squares (See the end of Section 4.2). It also generates a non-negative fresh variable $y_{0}$. If $\psi$ is strict, the algorithm adds the constraint $y_{0}>0.$ Finally, the algorithm symbolically computes

and equates the corresponding coefficients in the LHS and RHS to obtain QP constraints.

$\Phi$ is unsatisfiable due to the first condition of Theorem 4.6: This case is handled similary to case (1) above, except that we have $-1=y_{0}+h_{0}+\sum_{i=1}^{r}h_{i}\cdot f_{i}.$