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.
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.
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.
(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.