checkpred - utility to create and verify logical formulas for determining whether a given inequality is redundant after eliminating variables, without eliminating the variables.
The input file is a list of inequalities defining a polyhedron P in lrs format 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. checkpred is a utility for determining this without performing the projection. It produces logical formulas in SMT-LIB 2.6 format that are satisfiable iff the I is non-redundant for the projection. In addition, checkpred can produce lrs inputs that verify witnesses of non-redundancy produced by an SMT solver.
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 checkpred and required.
The output is in SMT-LIB 2.6 format using logic LRA. Solvers such as z3 or cvc4 support this logic. See The SMT-LIB Standard: Version 2.6 for details.
checkpred [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.
checkpred -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.
checkpred -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.
(1) Check if the first inequality in cp4.ine is redundant for projections.
(a) To check for redunancy after the first variable is eliminated, add options "redund_list 1 1" and "eliminate 1 1" to cp4.ine. Then:
% checkpred cp4.ine > cp4-11.smt
% z3 cp4-11.smt > cp4-11.out
% cvc4 -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:
% checkpred -c 1 cp4.ine < cp4-11.out | lrs
% checkpred -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
% checkpred cp4.ine > cp4-112.smt
% z3 cp4-112.smt > cp4-112.out
% cvc4 -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.
- SMT-Lib Standards
Charles Jordan <skip at res dot otaru-uc dot ac dot jp >