Check an LP certificate

A linear program’s optimum comes with a certificate: the plan, and a price for each constraint. lein lp-view checks that pair with Rainbow’s LP certificate checker and writes the LP Certificate Viewer, a page that shows each comparison the proof is built from. The verdict is the kernel’s check of one instance of optimization/signed-lp-optimality-certificate-on.

You need a clone at v1.5.5 (Install).

Write the instance and the certificate

Two products share two limits. Each unit of either product uses one unit of the first limit (4 available), and the first product also uses one unit of the second (3 available). The first earns 2 per unit; the second loses 1. Numbers are exact rationals. certify and bound compute exactly with numbers beyond a Java long since 1.5.3, and so does lein lp-view, which computes its own step-by-step values, since 1.5.4 (CHANGELOG). Since 1.5.5 the checker’s cost estimate depends only on the instance’s shape (rows, columns, equalities), so number size and zero entries no longer count against the budget. When the estimate does refuse a certificate, lein lp-view says the certificate was not checked because the estimate exceeded the budget, and names the library route that checks it without the estimate ({:preflight? false}) (CHANGELOG).

/tmp/instance.edn:

{:matrix [[1 1] [1 0]] :capacities [4 3] :margins [2 -1]}

/tmp/certificate.edn, a plan and a price per limit:

{:plan [3 0] :prices [0 2]}

Without :sense, the problem is to maximise. Minimisation and equality rows are supported too; see rainbow.view.lp in the repository.

Check it

lein lp-view /tmp/instance.edn /tmp/certificate.edn /tmp/lp-ok

wrote /tmp/lp-ok/index.html and lp-view.json; certify: certified 6

The plan earns 6, and the exit code is 0. Open /tmp/lp-ok/index.html. For each limit, the page shows its use (3 of 4, and 3 of 3), its slack and its price. For each product, it shows the price of its column against its margin. It also shows both objectives, 6 and 6, so the gap is 0. Every one of those numbers is confirmed by its own kernel check. The page also runs negative controls, the same checks with a number off by one, and they must be refused, or nothing is written.

Change one price

Lower the price of the second limit from 2 to 1. /tmp/tampered.edn:

{:plan [3 0] :prices [0 1]}

lein lp-view /tmp/instance.edn /tmp/tampered.edn /tmp/lp-bad

wrote /tmp/lp-bad/index.html and lp-view.json; certify: rejected -- first failing step: x1, column price 1 >= margin 2 -- kernel category :kernel/type-mismatch (Milestone declaration rejected)

The exit code is 1. The line and the page name the comparison that failed: the prices no longer cover the first product’s margin, and the gap between the objectives is −3.

Data of the wrong shape

certify checks the shape of what it certifies before any other work. A plan with an extra entry, /tmp/extra.edn:

{:plan [3 0 7] :prices [0 2]}

lein lp-view /tmp/instance.edn /tmp/extra.edn /tmp/lp-extra

FAIL lp-view /tmp/instance.edn /tmp/extra.edn -- :plan must have 2 entries (one per column, as :margins), but it has 3. The certificate would otherwise be checked on a different vector than the one submitted. (:lp-certificate/shape-mismatch) -- Check that :plan has one entry per column (:margins), :prices one per row (:capacities), each :matrix row one per column, and that every number is an exact rational such as 3 or 3/2.

The exit code is 1, and nothing is written. A floating-point entry such as 3.0 is refused the same way (:lp-certificate/not-rational), and so is a :sense other than :maximize or :minimize (:lp-certificate/unknown-sense) (CHANGELOG). Since 1.5.4, so is an instance key it does not know, and the message names the nearest known one: unknown instance key :sence; did you mean :sense? (:lp-certificate/unknown-key) (CHANGELOG).

Next

• Explore a proof: the Proof Explorer.
• Commands: lein lp-view and the other commands.