polyv(1)

💖 polyv(1) — the group chat guide to polyv 💖

okay bestie, sit down, hydrate, because today we're learning polyv, from the polyv 7.3 era, and honestly? she's iconic. she's the utility that creates and verifies logical formulas checking properties of given H/V representations using logic solvers. that's the whole job. that's the vibe. periodt. ✨

---

✨ Name ✨

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

---

✨ Synopsis ✨

polyv [input-files]

that's it. that's the whole synopsis. lowkey elegant. 💅

---

✨ Description ✨

so 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 the number of input files you hand her. fr fr.

ngl, in many cases it's easier and faster to just use lrs, mplrs or other tools to check these questions directly. no cap. polyv is an alternative approach, and she's intended for some examples where the direct approach is difficult. she's the girl you call when the normal way is giving struggle. 🫶

okay so here's what she can do:

• One H-representation. 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's 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. plus, polyv it produce lrs inputs that verify witnesses of non-redundancy produced by an SMT solver. (yes we're keeping that sentence exactly, she said what she said 💀)
• Two representations. 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. 🔥
• Three representations. 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)) and it's made of:

1. an H-representation of a polyhedron,
2. a projection to a subset of variables given by the project or eliminate options, and
3. an inequality to test given by the redund or redund_list options.

🚨 bestie, listen to me: only "linearity", "redund", "redund_list", "project" and "eliminate" options are supported. that's the whole list. nothing else. and the combination of redund/redund_list and project/eliminate options is both unique to polyv and required. required, bestie. you cannot skip it. 💅

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. (she's quiet like that. 🙈)

a witness of non-redundancy can be verified using two certificates. here's the tea:

• 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) 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 the second is infeasible, so the witness proves non-redundancy for the projection. slay. 💅

(b) redundancy 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. she said no witness, bestie. 😭

(2) check if given H- and V-representations define different polyhedra 🌈

(a) mp5.ine vs mp5.ext

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 — http://smtlib.cs.uiowa.edu/language.shtml
2. z3 — https://github.com/Z3Prover/z3/wiki
3. cvc5 — https://cvc5.github.io/

---

👑 Author 👑

Charles Jordan <skip at res dot otaru-uc dot ac dot jp > — we stan. 🫶

---

🔗 See also 🔗

lrslib(5), lrs(1)

---

and that's the whole page, bestie!! this one dropped October 2023, from the 2023.10.21 release of polyv 7.3, and honestly she ate and left no crumbs. go verify some witnesses. mwah. 💖✨🎀🦋🌸💅