1checkpred(1)                     checkpred 7.2                    checkpred(1)
2
3
4
5   Name
6       checkpred - utility to create and verify logical formulas for
7       determining whether a given inequality is redundant after eliminating
8       variables, without eliminating the variables.
9
10   Synopsis
11       checkpred [input-file]
12
13   Description
14       The input file is a list of inequalities defining a polyhedron P in lrs
15       format along with a list of variables for a projection of P and an
16       inequality I to test. The question is whether we have the same
17       projection when I is deleted from P.  If so we say I is redundant for
18       the projection, otherwise it is non-redundant.  checkpred is a utility
19       for determining this without performing the projection.  It produces
20       logical formulas in SMT-LIB 2.6 format that are satisfiable iff the I
21       is non-redundant for the projection.  In addition, checkpred can
22       produce lrs inputs that verify witnesses of non-redundancy produced by
23       an SMT solver.
24
25
26   File formats
27       The input file is in lrs format (see lrs(1)) consisting of (a) an H-
28       representation of a polyhedron, (b) a projection to a subset of
29       variables given by the project or eliminate options, and (c) an
30       inequality to test given by the redund or redund_list options.  Note
31       that only "linearity", "redund", "redund_list", "project" and
32       "eliminate" options are supported, and the combination of
33       redund/redund_list and project/eliminate options is both unique to
34       checkpred and required.
35
36
37       The output is in SMT-LIB 2.6 format using logic LRA.  Solvers such as
38       z3 or cvc4 support this logic.  See The SMT-LIB Standard: Version 2.6
39       for details.
40
41
42   Options
43       checkpred [input-file] produces a logical formula satisfiable iff the
44       first inequality given in a redund/redund_list option is redundant
45       after projection according to a project/eliminate option.  The solver
46       can produce witnesses for non-redundant inequalities, i.e.  an
47       assignment to the variables whose image is in the projection only if
48       the inequality is removed.  No witness is produced if the inequality is
49       redundant.
50
51       A witness of non-redundancy can be verified using two certificates.
52       The first certificate specifies that the assignment to the variables is
53       feasible when the inequality in question is removed.  The second
54       certificate asserts that when this inequality is added, no feasible
55       assignment has the same projection.  Certificates are produced using
56       the following options.
57
58       checkpred -c 1 [input-file] reads a witness of non-redundancy on
59       standard input and produces an lrs input file that should be feasible.
60       The options in the input file should be the same as when the formula
61       was produced.
62
63
64       checkpred -c 2 [input-file] reads a witness of non-redundancy on
65       standard input and produces an lrs input file that should be
66       infeasible.  The options in the input file should be the same as when
67       the formula was produced.
68
69
70   Examples
71       (1) Check if the first inequality in cp4.ine is redundant for
72       projections.
73       (a) To check for redunancy after the first variable is eliminated, add
74       options "redund_list 1 1" and "eliminate 1 1" to cp4.ine. Then:
75
76        % checkpred cp4.ine > cp4-11.smt
77        % z3 cp4-11.smt > cp4-11.out
78       or
79        % cvc4 -L smt --produce-models cp4-11.smt > cp4-11.out
80
81       The first line of cp4-11.out reads "sat" indicating that inequality 1
82       is non-redundant for eliminating variable 1. We can check the witness:
83
84        % checkpred -c 1 cp4.ine < cp4-11.out | lrs
85        % checkpred -c 2 cp4.ine < cp4-11.out | lrs
86
87       The first certificate is feasible and second infeasible, so the witness
88       proves non-redundancy for the projection.
89       (b) To check for redunancy after variables 1 and 2 are eliminated, add
90       options "redund_list 1 1" and "eliminate 2 1 2" to cp4.ine. Then
91
92        % checkpred cp4.ine > cp4-112.smt
93        % z3 cp4-112.smt > cp4-112.out
94       or
95        % cvc4 -L smt --produce-models cp4-112.smt > cp4-112.out
96
97       The first line of cp4-112.out reads "unsat" indicating that inequality
98       1 is redundant for eliminating variables 1 and 2.  In this case there
99       is no witness.
100
101
102   Notes
103        1. SMT-Lib Standards
104           http://smtlib.cs.uiowa.edu/language.shtml
105
106        2. z3
107           https://github.com/Z3Prover/z3/wiki
108
109        3. cvc4
110           https://cvc4.github.io/
111
112   Author
113       Charles Jordan <skip at res dot otaru-uc dot ac dot jp >
114
115   See also
116       lrslib(5), lrs(1)
117
118
119
120September 2020                     2020.9.28                      checkpred(1)
Impressum