## table of contents

- unstable 0.73-2
- experimental 0.73-1

polyv(1) | polyv 7.3 | polyv(1) |

## Name¶

polyv - utility to create and verify logical formulas checking properties of given H/V representations using logic solvers.

## Synopsis¶

**polyv** *[input-files]*

## Description¶

The input file or files are H- or V-representations of polyhedra
in *lrs* format, and the output is a logical formula in *SMT-LIB*
2.6 format. Behavior depends on the options and number of input files
provided. In many cases, it is easier and faster to use *lrs*,
*mplrs* or other tools to check the following questions directly.
*polyv* is an alternative approach intended for some examples where the
direct approach is difficult.

First, *polyv* can be given a single H-representation
defining a polyhedron P, along with a list of variables for a projection of
P and an inequality I to test. The question is whether we have the same
projection when I is deleted from P. If so we say I is redundant for the
projection, otherwise it is non-redundant. *polyv* allows the use of
SMT solvers to decide this question without performing the projection
explicitly, producing a formula that is satisfiable iff the I is
non-redundant for the projection. In addition, *polyv* it produce
*lrs* inputs that verify witnesses of non-redundancy produced by an SMT
solver.

Next, *polyv* can be given two representations defining
polyhedra P and Q, where H-representations may contain projections. The
question is whether P and Q are different polyhedra: *polyv* produces a
formula that is satisfiable iff there is a point contained in exactly one of
P and Q.

Finally, *polyv* can be given three representations defining
polyhedra P, Q and R. The question is whether the intersection of P and Q is
different from R: *polyv* produces a formula that is satisfiable iff
there is a point contained in exactly one of R and the intersection.

## File formats¶

The input file is in *lrs* format (see lrs(1)**)**
consisting of (a) an H-representation of a polyhedron, (b) a projection to a
subset of variables given by the *project* or *eliminate* options,
and (c) an inequality to test given by the *redund* or
*redund_list* options. Note that only "linearity",
"redund", "redund_list", "project" and
"eliminate" options are supported, and the combination of
redund/redund_list and project/eliminate options is both unique to polyv and
required.

The output is in *SMT-LIB* 2.6 format using logic *LRA*.
Solvers such as *z3* or *cvc5* support this logic. See The SMT-LIB
Standard: Version 2.6 for details.

## Usage¶

**polyv** [input-file] produces a logical formula
satisfiable iff the first inequality given in a redund/redund_list option is
redundant after projection according to a project/eliminate option. The
solver can produce witnesses for non-redundant inequalities, i.e. an
assignment to the variables whose image is in the projection only if the
inequality is removed. No witness is produced if the inequality is
redundant.

A witness of non-redundancy can be verified using two certificates. The first certificate specifies that the assignment to the variables is feasible when the inequality in question is removed. The second certificate asserts that when this inequality is added, no feasible assignment has the same projection. Certificates are produced using the following options.

**polyv** -c 1 [input-file] reads a witness of
non-redundancy on standard input and produces an lrs input file that should
be feasible. The options in the input file should be the same as when the
formula was produced.

**polyv** -c 2 [input-file] reads a witness of
non-redundancy on standard input and produces an lrs input file that should
be infeasible. The options in the input file should be the same as when the
formula was produced.

**polyv** [input-file-1] [input-file-2] given two H/V
representations, produces a logical formula satisfiable iff they define
different polyhedra. Projections are supported in H-representations using
the project or eliminate option. This can be used to e.g. verify H/V
equivalency or fel projections.

**polyv** [input-file-1] [input-file-2] [input-file-3]
given three H/V representations, produces a logical formula satisfiable iff
the intersection of polyhedra defined by input-file-1 and input-file-2 is
not defined by input-file-3. Projections are supported in H-representations
using the project or eliminate option.

## Examples¶

(1) Check if the first inequality in cp4.ine is redundant for
projections.

(a) To check for redundancy after the first variable is eliminated, add
options "redund_list 1 1" and "eliminate 1 1" to
cp4.ine. Then:

% polyv cp4.ine > cp4-11.smt

% z3 cp4-11.smt > cp4-11.out

or

% cvc5 -L smt --produce-models cp4-11.smt > cp4-11.out

The first line of cp4-11.out reads "sat" indicating that inequality 1 is non-redundant for eliminating variable 1. We can check the witness:

% polyv -c 1 cp4.ine < cp4-11.out | lrs

% polyv -c 2 cp4.ine < cp4-11.out | lrs

The first certificate is feasible and second infeasible, so the
witness proves non-redundancy for the projection.

(b) To check for redunancy after variables 1 and 2 are eliminated, add options
"redund_list 1 1" and "eliminate 2 1 2" to cp4.ine.
Then

% polyv cp4.ine > cp4-112.smt

% z3 cp4-112.smt > cp4-112.out

or

% cvc5 -L smt --produce-models cp4-112.smt > cp4-112.out

The first line of cp4-112.out reads "unsat" indicating that inequality 1 is redundant for eliminating variables 1 and 2. In this case there is no witness.

(2) Check if given H- and V- representations define different
polyhedra.

(a) To check whether mp5.ine and mp5.ext (produced using lrs) define different
polyhedra:

% polyv mp5.ine mp5.ext > mp5hv.smt

% z3 mp5hv.smt > mp5hv.out

The first line of mp5hv.out reads "unsat" indicating
that these two representations do not define different polyhedra (i.e. they
are equivalent).

(b) After removing the last vertex (the origin) from mp5.ext to create

mp5missing.ext:

% polyv mp5.ine mp5missing.ext > mp5hvm.smt

% z3 mp5hvm.smt > mp5hvm.out

The first line of mp5hvm.out reads "sat" indicating that
these two representations define different polyhedra.

Note that the H-representations are allowed to include projections.

## Notes¶

- 1.
- SMT-Lib Standards

- 2.
- z3

- 3.
- cvc5

## Author¶

Charles Jordan <skip at res dot otaru-uc dot ac dot jp >

## See also¶

**lrslib**(5), lrs(1)

2023.10.21 | October 2023 |