# polyv - Man Page

### 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

### Author

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