Farkas certificates and minimal witnesses
329
Certificates for universally-quantified statements. In order to deal with
the cases (1) and (3), we need the following lemma proved in the full version [42].
Lemma 3.1. For A ∈ R
M×S
, b ∈ R
M as in Setting 2.2, we have for all z ∈ R
S :
Az ≤ b =⇒ z ≤ Pr
min (♦ goal)
Az ≥ b =⇒ z ≥ Pr
max (♦ goal)
Corollary 3.2. For ∈ {≥, >} and ∈ {≤, <} we have
Pr
min
s0 (♦ goal) λ ⇐⇒ ∃z ∈ R
S
. Az ≤ b ∧ z(s 0 ) λ
Pr
max
s0 (♦ goal) λ ⇐⇒ ∃z ∈ R
S
. Az ≥ b ∧ z(s 0 ) λ
Proof. For the direction from left to right, we take z to be Pr
min (♦ goal). The
opposite direction follows from Lemma 3.1.
The right hand sides of Corollary 3.2 provide certifying formulations for problems (1) and (3): to check whether the corresponding threshold statement holds,
one must merely check whether z satisfies the inequalities, rather than checking
whether Pr
min / max
s0
(♦ goal) was computed correctly. If the threshold condition is
satisfied, then the vectors Pr
min / max
s0
(♦ goal) are also valid certificates.
Certificates for existentially-quantified statements. To find certificates
for the cases (2) and (4), we calculate:
Pr
min
s0 (♦ goal) < λ
Cor. 3.2
⇐⇒ ¬ ∃z ∈ R
S
≥0 . Az ≤ b ∧ z(s 0 ) ≥ λ
⇐⇒ ¬ ∃z ∈ R
S
≥0 .
⎛
⎝
A
−1 0 . . . 0
⎞
⎠ z ≤
⎛
⎝
b
−λ
⎞
⎠
Lem. 2.1
⇐⇒
∃y ∈ R
M
≥0 , y
∗
≥ 0. (y, y
∗ )
⎛
⎝
A
−1 0 . . . 0
⎞
⎠ ≥ 0 ∧ (y, y
∗ )
⎛
⎝
b
−λ
⎞
⎠ < 0
⇐⇒ ∃y ∈ R
M
≥0 . yA ≥ δ s0 ∧ yb < λ.
For non-strict inequalities, we apply Farkas’ Lemma in the opposite direction:
Pr
min
s0 (♦ goal) ≤ λ
Cor. 3.2
⇐⇒ ¬ ∃z ∈ R
S
≥0 . Az ≤ b ∧ z(s 0 ) > λ
⇐⇒ ¬ ∃z ∈ R
S
≥0 , z
∗
≥ 0.
−A b
⎛
⎝
z
z
∗
⎞
⎠ ≥ 0 ∧
−δ s0 λ
⎛
⎝
z
z
∗
⎞
⎠ < 0
Lem. 2.1
⇐⇒
∃y ∈ R
M
≥0 . y
−A b
≤
−δ s0 λ
⇐⇒ ∃y ∈ R
M
≥0 . yA ≥ δ s0 ∧ yb ≤ λ.
The deductions for Pr
max (♦ goal) are analogous, so that we get: