SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PFEModule

Implements factor elimination in polynomials based on factorization and variable bounds.

Given a constraint $p \sim 0$ with $\sim \in \{ =, \neq, \geq, >, \leq, < \}$ and bounds $b$ on the variables in $p$, the module does the following: It computes a factor $q$ such that $p = q \cdot r$ and evaluates $q$ on the intervals represented by the bounds. If the resulting interval $q(b)$ if sign-invariant, the constraint can be simplified or additional constraints can be added. We consider an interval to be sign-invariant, if it is positive, semi-positive, zero, semi-negative or negative.

Simplifications

The following simplifications are done for for $q \cdot r \sim 0$:

$\sim$ $q(b) > 0$ $q(b) \geq 0$ $q(b) = 0$ $q(b) < 0$ $q(b) \leq 0$
$=$ $p := r$ $f := q=0 \vee r=0$ $p := 0$ $p := r$ $f := q=0 \vee r=0$
$\neq$ $p := r$ $f := q>0 \wedge r \neq 0$ $p := 0$ $p := r$ $f := q<0 \wedge r \neq 0$
$\geq$ $p := r$ $f := q=0 \vee r \geq 0$ $p := 0$ $c := r \leq 0$ $f := q=0 \vee r \leq 0$
$>$ $p := r$ $f := q>0 \wedge r>0$ $p := 0$ $c := r<0$ $f := q<0 \wedge r<0$
$\leq$ $p := r$ $f := q=0 \vee r \leq 0$ $p := 0$ $c := r \geq 0$ $f := q=0 \vee r \geq 0$
$<$ $p := r$ $f := q>0 \wedge r<0$ $p := 0$ $c := r>0$ $f := q<0 \wedge r>0$

Notation: $p := p'$ replaces the polynomial, $c := p' \sim 0$ replaces the whole constraint by a new one and $f := f'$ replaces the constraint by a new formula.

To maximize the cases where $q(b)$ actually is sign-invariant, we proceed as follows. We compute a factorization of $p$, that is a number of polynomials $p_i$ such that $p = \prod_{i=1}^k p_i$. We now separate all $p_i$ into two sets: $P_q$ for all sign-invariant $p_i$ and $P_r$ for all other $p_i$. Thereby, we set $q = \prod_{t \in P_q} t$ and $r = \prod_{t \in P_r}$ and know that $q(b)$ is sign-invariant.

Instead of computing $q(b)$ once again afterwards, we can determine the type of sign-invariance of $q(b)$ from the types of sign-invariances of the factors from $P_q$. Assume that we start with a canonical factor $1$ and a sign-invariance of $>$, we can iteratively combine them like this:

Combining types of sign-invariance

Combining two types of sign-invariance is done as follows:

$\cdot$ $>$ $\geq$ $=$ $\leq$ $<$
$>$ $>$ $\geq$ $=$ $\leq$ $<$
$\geq$ $\geq$ $\geq$ $=$ $\leq$ $\leq$
$=$ $=$ $=$ $=$ $=$ $=$
$\leq$ $\leq$ $\leq$ $=$ $\geq$ $\geq$
$<$ $<$ $\leq$ $=$ $\geq$ $>$