Explicit description of quasi-symmetric solution set:
computer-assisted proof of superfluous inequalities

Evgenija D. Popova

Institute of Mathematics and Informatics
Bulgarian Academy of Sciences
Acad. G. Bonchev  str., block 8
1113 Sofia, Bulgaria
epopova@math.bas.bg

Consider the linear algebraic system A(p)x=b(p),
where the input data are linear functions of interval parameters.
Characterizing the so-called united parametric solution set by inequalities not
involving the interval parameters is a fundamental problem of considerable practical importance.
The problem is related to quantifier elimination which stimulated
a tremendous amount of research. Since Tarski's general theory
is EXPSPACE-hard, a lot of research is devoted to special cases with polynomial-time decidability. 

In this work we present explicit description of the symmetric solution set obtained by 
an improved Fourier-Motzkin-type elimination of parameters.
In fact, we consider a slight generalization of the classical linear system with a symmetric matrix. 
The generalized system can contain in the diagonal elements of the matrix and in the
right-hand side vector numerical values and an arbitrary but fixed
number of parameters, each involved in only one equation. 
We call this system  quasi-symmetric and search for a description of its solution set.

We apply an improved Fourier-Motzkin-type parameter elimination
process (see Popova, BIT 2012) and some sufficient conditions
(proven therein) for detecting superfluous or redundant characterizing
inequalities. Nevertheless, the parameter elimination  process still generates an exponential number of 
redundant characterizing inequalities. We have developed a methodology which detects all 
superfluous or redundant inequalities in the description of the quasi-symmetric solution set. 
The methodology is constructive in the sense that it allows computer-assisted proof of the 
superfluous or redundant inequalities. 

The explicit description of quasi-symmetric solution set is based on this methodology and involves 
3^n/2 - 2^n + 1/2  inequalities, where n is the dimension of the system.