., White-Box, White-Box. White-Box.,, White-Box., Maple [11], 2. 1, QE, QE, 1 Redlog [7], QEPCAD [9], SyNRAC [8] 3 QE., 2 Brown White-Box. 3 White-Box

Transcription

1 White-Box Takayuki Kunihiro Graduate School of Pure and Applied Sciences, University of Tsukuba Hidenao Iwane ( ) / Fujitsu Laboratories Ltd. / National Institute of Informatics. Yumi Wada Graduate School of Pure and Applied Sciences, University of Tsukuba Akira Terui Faculty of Pure and Applied Sciences, University of Tsukuba 1, (Quantifier Elimination; QE) ([1], [5]). QE. QE, QE. (Virtual Substituition) [10], QE., QE QE. QE,,,,, QE., ([3], [12]). C. W. Brown, A. Strzeboński White-Box [4].,,, hirophirop@gmail.com iwane@jp.fujitsu.com wada.yumi.ww@alumni.tsukuba.ac.jp terui@math.tsukuba.ac.jp 1

2 ., White-Box, White-Box. White-Box.,, White-Box., Maple [11], 2. 1, QE, QE, 1 Redlog [7], QEPCAD [9], SyNRAC [8] 3 QE., 2 Brown White-Box. 3 White-Box, 4 White-Box. 2 White-Box, Brown and Strzeboński [4] White-Box., Brown White-Box,. 2.1 White-Box,,. 1 ( ) p, φ(p), φ(p) {p = 0, p 0, p < 0, p 0, p > 0, p 0, true, false}., true, false, 0 = 0, true, false,,. 2 ( OP) OP 8. R, { true, false }. 1. NOOP(x) false. 2. LTOP(x) true if x < 0, else false. 3. LEOP(x) true if x 0, else false. 4. GTOP(x) true if x > 0, else false. 5. GEOP(x) true if x 0, else false. 6. EQOP(x) true if x = 0, else false. 7. NEOP(x) true if x 0, else false. 8. ALOP(x) true., x > 0 GTOP(x 2 + 1). Q Z[x 1,..., x n ] α : Q OP, x. α(q)(q(x)).., { LTOP (q = x + y) Q = {x + y, x y}, α(q) = GEOP (q = x y), x + y < 0 x y 0., OP. q Q 2

3 3 (OP ) OP +,, : OP OP OP. (α + β)(z) true if x, y [z = x + y α(x) β(y)], else false. (αβ)(z) true if x, y [z = xy α(x) β(y)], else false. (α β)(z) true if [α(z) β(z)], else false., S Q : OP OP. S Q(α)(z) true if x[z = x 2 α(x)], else false. 4 ( OP) sgn: R OP. LTOP (x < 0) sgn(x) EQOP (x = 0) GTOP (x > 0) 5 (PP(x 1,..., x n )) Z[x 1,..., x n ] *2, *3 PP(x 1,... x n ). 6 ( ) a OP, b OP, x[a(x) b(x)], a b. 2.2 White-Box. 1 y 2 x + 1 > 0 2x 1 < 0. y 2 x + 1 > 0 2x 1 < 0 y x 1 > 0 2x 1 < 0 2 2x 1 < 0 ϕ 1 y 2 x + 1 > 0, ϕ 2 2x 1 < 0., ϕ 1 2, 3 2x 1 2 ϕ y , ϕ 2 ϕ 1, ϕ 1 ϕ 2 ϕ 2. White-Box,, 1. 2x 1 < 0 y 2 x + 1. White-Box. White-Box 2.,, PolynomialSign, Algorithm 2. PolynomialSign, Algorithm 1, MonomialSign., 2 p, q, q, p, DeduceSign, Algorithm 4. DeduceSign, Algorithm 3, FindInterval. *2 1 *3 Cox, Little and O Shea [6, 2, 3]., x 1,..., x n a, b,..., y, z x 1 > x 2 > > x n, a > b > > y > z. 3

4 Algorithm 1 MonomialSign [4, Algorithm 2] Input: M = x e xe n n :, α 1,..., α n OP Output: β OP s.t. α 1 (x 1 ) α n (x n ) β(m) 1: β GTOP 2: for 1 i n do 3: if e i : even then β S Q(α i ) β else β α i β end if 4: end for 5: return β Algorithm 2 PolynomialSign [4, Algorithm3] Input: p = a 1 M a k M k Z[x 1,..., x n ] (M i x 1,..., x n ), α 1,..., α n OP Output: β OP s.t. α 1 (x 1 ) α n (x n ) β(p) 1: β EQOP 2: for 1 i k do 3: β sgn(a i ) MonomialSign(M i ; α 1,..., α n ) + β 4: end for 5: return β 2 1, p = y 2 x + 1, q = 2x 1, α(x) = ALOP, α(y) = ALOP, β = LTOP DeduceSign., 2x 1 < 0 y 2 x FindIntervals I 1 = { 1 2}, I2 =, strict = true. ( p q > 0. ) 2. β = LTOP I 1 R +, DeduceSign 3, 4, γ = GTOP. 2x 1 < 0, y 2 x + 1 > 0. 1, 1 DeduceSign,, 1 DeduceAll, Algorithm 5. DeduceAll,,, DeduceAllSigns, Algorithm White-Box, Brown White-Box Algorithm 7., White-Box P PP(x 1,..., x n ), σ: P OP p P σ p (p). White-Box 5. 1., (1 10 ) 2.,. (12 15 ) 3. 2, 2 (11, 16 ) 4., () (17 31 ) 5. (32 36 )

5 Algorithm 3 FindIntervals [4, Algorithm 4] Input: p = a 1 M a k M k, q = b 1 M b k M k Z[x 1,..., x n ], α 1,..., α n OP Output: I 1, I 2 : R, strict { true, false } s.t., strict = true α 1 (x 1 ) α n (x n ) t I 1 [p + tq 0] t I 2 [p + tq 0], α 1 (x 1 ) α n (x n ) t int(i 1 )[p + tq > 0] t int(i 2 )[p + tq < 0]., int(i 1 ), int(i 2 ) I 1, I 2. 1: I 1 R, I 2 R, strict false 2: for 1 i k do 3: s MonomialSign(M i ; α 1,..., α n ) 4: if s = NOOP then I 1 end if 5: if s = LEOP s = LTOP then 6: if s = LTOP then strict true end if 7: if = 0 a i < 0 then I 2 8: else if = 0 a i > 0 then I 1 9: else if < 0 then I 1 I 1 [ a i, ), I 2 I 2 (, a i ] 10: else if > 0 then I 1 I 1 (, a i ], I 2 I 2 [ a i, ) 11: end if 12: else if s = GEOP s = GTOP then 13: if s = GTOP then strict true end if 14: if = 0 a i < 0 then I 1 15: else if = 0 a i > 0 then I 2 16: else if < 0 then I 1 I 1 (, a i ], I 2 I 2 [ a i, ) 17: else if > 0 then I 1 I 1 [ a i, ), I 2 I 2 (, a i ] 18: end if 19: else if s = NEOP s = ALOP then 20: if = 0 a i 0 then I 1, I 2, else I 1 I 1 { a i }, I 2 I 2 { a i } end if 21: end if 22: end for 23: return I 1, I 2, strict 1. p q, q 0 p p PolynomialSign. 3. p DeduceAll.,,. White-Box. 3 White-Box White-Box., White-Box 3.,, 5

6 Algorithm 4 DeduceSign [4, Algorithm 5] Input: p = a 1 M a k M k, q = b 1 M b k M k Z[x 1,..., x n ], α 1,..., α n, β OP Output: γ OP s.t. α 1 (x 1 ) α n (x n ) β(q) γ(p) 1: γ ALOP, (I 1, I 2, strict) FindIntervals(p; q; α 1,..., α n ) 2: if β = LTOP then 3: if I 1 R + then γ GTOP else if 0 I 1 then γ GEOP end if 4: if I 2 R then γ γ LTOP else if 0 I 2 then γ γ LEOP end if 5: else if β = LEOP then 6: if strict and int(i 1 ) R + then γ GTOP else if I 1 (R + {0}) then γ GEOP end if 7: if strict and int(i 2 ) R then γ γ LTOP else if I 2 (R {0}) then γ γ LEOP end if 8: else if β = GTOP then 9: if I 1 R then γ GTOP else if 0 I 1 then γ GEOP end if 10: if I 2 R + then γ γ LTOP else if 0 I 2 then γ γ LEOP end if 11: else if β = GEOP then 12: if strict and int(i 1 ) R then γ GTOP else if I 1 (R {0}) then γ GEOP end if 13: if strict and int(i 2 ) R + then γ γ LTOP else if I 2 (R + {0}) then γ γ LEOP end if 14: else if β = EQOP then 15: if strict and int(i 1 ) then γ GTOP else if I 1 then γ GEOP end if 16: if strict and int(i 2 ) then γ γ LTOP else if I 2 then γ γ LEOP end if 17: end if 18: return γ Algorithm 5 DeduceAll [4, Algorithm 6] Input: p = a 1 M a k M k, Q Z[x 1,..., x n ], α 1,..., α n OP, β : Q q β q OP Output: γ OP s.t. α 1 (x 1 ) α n (x n ) q Q β q (q) γ(p) 1: γ ALOP 2: for all q Q do 3: if β q NEOP β q ALOP then 4: γ γ DeduceSign(p; q; α 1,..., α n ; β q ) 5: if γ = NOOP then return NOOP end if 6: end if 7: end for 8: return γ White-Box (Algorithm 7) AndSimplify., ψ Ψ ψ (Ψ: ), ϕ Φ ϕ (Φ: ).,. 3.1 AndSimplify.. (), () 6

7 Algorithm 6 DeduceAllSigns [4, Algorithm 7] Input: P, Q Z[x 1,..., x n ], α 1,..., α n OP, β : P p β p OP, γ : Q q γ q OP Output: α 1,..., α n OP, β : P p β p OP, unsat {true, false} s.t. if unsat = true, F false, else F α 1 (x 1 ) α n (x n ) p P β p (p) q Q γ q (q) (F α 1 (x 1 ) α n (x n ) p P β p (p) q Q γ q (q)) 1: unsat false, R P Q. for 1 i n do α i α i end for. for all p P do β p β p end for. 2: for all r R do 3: if r P then δ r β r else δ r γ r end if 4: end for 5: for all 1 i n do 6: α i α i DeduceAll(x i ; R; α 1,..., α n ; δ) 7: if α i = NOOP then unsat true end if 8: end for 9: for all p P do 10: R R \ {p}, δ δ R, β p β p DeduceAll(p; R; α 1,..., α n ; δ) 11: if β p = NOOP then unsat true end if 12: end for 13: return α 1,..., α n, β, unsat, AndSimplify. Input = φ(p) p P φ(p) p P ψ(p), ψ(p), AndSimplify φ(p) p P p P p P ψ(p) = Output. p P (1) OrSimplify. OrSimplify OP. 7 (OP ) NEG : OP OP NEG(op)(x) true if (op(x)), else false., op OP. OrSimplify Algorithm 8., OrSimplify P PP(x 1,..., x n ), σ: P OP p P σ p (p)., unsat AndSimplify. unsat = true, AndSimplify false, OrSimplify true. 3 ψ y 2 x x 1 0 OrSimplify. (1), ψ y 2 x x 1 0 (y 2 x + 1 > 0 2x 1 < 0) (2x 1 < 0) ( 1) 2x 1 0, ψ. 7

8 Algorithm 7 White-Box (AndSimplify) [4, Algorithm 8] Input: P PP(x 1,..., x n ), σ : P p σ p OP Output: Q PP(x 1,..., x n ), τ : Q q τ q OP, unsat {true, false} s.t. if unsat = true, p P σ p (p) false, else p P σ p (p) q Q τ q (q) 1: Q P, τ σ, unsat false, P 1 P, P 2 P 1 \ {x 1,..., x n }, P 3 P \ P 1 2: for 1 i n do 3: if x i P then α i σ xi else α i ALOP end if 4: end for 5: for all p P 2 do 6: if p P then β p σ p else β p ALOP end if 7: β p β p PolynomialSign(p; α 1,..., α n ) 8: if β p = NOOP then unsat true, return Q, τ, unsat end if 9: end for 10: for all p P 3 do γ p σ p end for 11: repeat 12: changed false 13: (α 1,..., α n ), β, unsat DeduceAllSigns(P 2 ; P 3 ; α 1,..., α n ; β; γ) 14: if unsat = true then return Q, τ, unsat end if 15: if (α 1,..., α n ) (α 1,..., α n ) β β then (α 1,..., α n ) (α 1,..., α n ), β β, changed true end if 16: until changed = false 17: for all p P 2 do 18: if β p = NEOP p q P 3 γ q {LTOP, GTOP, NEOP} then β p ALOP end if 19: if β p ALOP β p = PolynomialSign(p; α 1,..., α n ) then β p ALOP end if 20: if β p ALOP then 21: R (P 2 \ {p}) P 3, ρ (β P 2 \ {p}) γ 22: if β p = DeduceAll(p; R; α 1,..., α n ; ρ) then β p ALOP end if 23: end if 24: end for 25: for all p P 3 do 26: if γ p ALOP γ p = PolynomialSign(p; α 1,..., α n ) then γ p ALOP end if 27: if γ p ALOP then 28: R P 2 (P 3 \ {p}), ρ β (γ P 3 \ {p}) 29: if γ p = DeduceAll(p; R; α 1,..., α n ; ρ) then γ p ALOP end if 30: end if 31: end for 32: Q 1 {x i α i ALOP}, Q 2 {p P 2 β p ALOP}, Q 3 {p P 3 γ p ALOP} Q Q 1 Q 2 Q 3 33: for all x i Q 1 do τ xi α i end for 34: for all p Q 2 do τ p β p end for 35: for all p Q 3 do τ p γ p end for 36: return Q, τ, unsat 8

9 Algorithm 8 OrSimplify Input: P PP(x 1,..., x n ), σ : P p σ p OP Output: Q PP(x 1,..., x n ), τ : Q q τ q OP, unsat { true, false } s.t. if unsat = true, p P σ p (p) true, else p P σ p (p) q Q τ q (q) 1: for all p P do σ p NEG(σ p ) end for 2: Q, τ, unsat AndSimplify(P; σ) 3: for all q Q do τ q NEG(τ q ) end for 4: return Q, τ, unsat 3.2 AndSimplify., AndSimplify. (p i, q j Z[x 1,..., x n ], φ(p i ), φ(q j ). ) t φ(q j ) (φ(p 1 ) φ(p s )) (2) j=1 t t (( φ(q j ) φ(p 1 )) ( φ(q j ) φ(p s ))) (3) j=1 j=1 j=1 t t (( φ(q j ) φ (p 1 )) ( φ(q j ) φ (p s ))) (4) j=1 t φ(q j ) (φ (p 1 ) φ (p s )). (5) j=1 (2), t j=1 φ(q j ) φ(p i ) ( (3)). (3) t j=1 φ(q j ) φ(p i ) DeduceAll. tj=1 φ(q j ) p i,. (4) ψ (p i ) ψ(p i )., t j=1 φ(q j ), φ(p i ) ( (5)). OrNestedSimplify, Algorithm 9., OrNestedSimplify P, Q PP(x 1,..., x n ), σ: P OP, τ: Q OP q Q τ q (q) p P σ p (p), 1, 2 P, σ, 3, 4 Q, τ. 4 φ 2x 1 < 0 (y 2 x z + 1 > 0) OrNestedSimplify. (2) (5), φ 2x 1 < 0 (y 2 x z + 1 > 0) (2x 1 < 0 y 2 x + 1 0) (2x 1 < 0 z + 1 > 0) (2x 1 < 0 false) (2x 1 < 0 z + 1 > 0) 2x 1 < 0 (false z + 1 > 0). false 2x 1 < 0 z + 1 > 0. 9

10 Algorithm 9 OrNestedSimplify Input: P PP(x 1,..., x n ), σ : P p σ p OP, Q PP(x 1,..., x n ), τ : Q q τ q OP (F q Q τ q (q) p P σ p (p). ) Output: R PP(x 1,..., x n ), σ : R r σ r OP. unsat { true, false } s.t. if unsat = true, F false, else F q Q τ q (q) (R r R σ r (r)) 1: R P, σ σ, unsat false 2: for 1 i n do 3: if x i Q then α i τ xi else α i ALOP end if 4: end for 5: for all r R do 6: for 1 i n do 7: if r = x i then α i σ r else α i α i end if 8: end for 9: if DeduceAll(r; Q; α 1,..., α n ; τ) σ r then R, σ, return R, σ, unsat 10: else σ r σ r DeduceAll(r; Q; α 1,..., α n ; τ) 11: end if 12: end for 13: if all σ r = NOOP then unsat true, return R, σ, unsat end if 14: R {r R σ r NOOP} 15: return R, σ, unsat OrNestedSimplify,, AndSimplify, OrSimplify. 4, AndSimplify OrSimplify, y 2 x + 1 0, z + 1 > 0, OrSimplify., y 2 x + 1 > 0., OrNestedSimplify, OrSimplify z + 1 > 0, 2x 1 < 0., OrNestedSimplify,,. 3.3., OrSimplify,, OrNestedSimplify. Input = ϕ ϕ Φ ϕ ϕ Φ ψ, ψ,ornestedsimplify ϕ ψ Ψ ψ Ψ ϕ Φ ψ = Output. ψ Ψ Algorithm 10 AndNestedSimplify., AndNestedSimplify P, Q PP(x 1,..., x n ), σ: P OP, τ: Q OP q Q τ q (q) p P σ p (p). 10

11 Algorithm 10 AndNestedSimplify Input: P PP(x 1,..., x n ), σ : P p σ p OP, Q PP(x 1,..., x n ), τ : Q q τ q OP (F q Q τ q (q) p P σ p (p). ) Output: R PP(x 1,..., x n ), σ : R r σ r OP. unsat { true, false } s.t. if unsat = true, F true, else F q Q τ q (q) (R r R σ r (r)) 1: for all p P do σ p NEG(σ p ) end for 2: for all q Q do τ q NEG(τ q ) end for 3: R, σ, unsat OrNestedSimplify(P; σ; Q; τ) 4: for all r R do σ r NEG(σ r ) end for 5: return R, σ, unsat, unsat OrNestedSimplify. unsat = true, OrNestedSimplify false, AndNestedSimplify true. 3.4 White-Box White-Box (AndSimplify), 3 (OrSimplify, OrNestedSimplify, AndNested- Simplify), White-Box (ExtendedWhite-Box) Algorithm 11. Algorithm 11,,, ϕ Φ ϕ ψ Ψ ψ (ϕ:, ψ: ), ϕ Φ ϕ ψ Ψ ψ (ϕ:, ψ: )., ϕ, ( ) ψ χ. ( ) ψ ( ) ω, Algorithm 11 (5, 23 ),, Algorithm 11 ω. 4 White-Box Maple, 2. 1 (QE ) SyNRAC QE, QE White-Box, QE White-Box ( White-Box + QE) 2. 2 ( QE ), Redlog (rlsimpl), QEPCAD (slfq), SyNRAC (synsimpl), White-Box 4,.. 11

12 Algorithm 11 ExtendedWhite-Box Input: F: Output: F : s.t. F F 1: if F = ϕ Φ ϕ ψ Ψ ψ (ϕ:, ψ: ) then 2: /* ψ ψ = χ X χ ω Ω ω (χ:, ω: ). */ 3: Φ Φ, Ψ Ψ 4: if Ψ then 5: ψ Ψ ψ ExtendedWhite-Box( ψ Ψ ψ) 6: /* ψ ψ = χ X χ ω Ω ω (χ :, ω : ) ψ Ψ ψ ψ Ψ ψ. */ 7: if ψ Ψ ψ : then Φ Φ { ψ Ψ ψ }, Ψ end if 8: end if 9: for all ψ Ψ do 10: /* P PP(x 1,..., x n ) σ: P p σ p OP p P σ p (p) = ϕ Φ ϕ. */ 11: /* Q PP(x 1,..., x n ) τ: Q q τ q OP q Q τ q (q) = χ X χ. */ 12: Q, τ, unsat AndNestedSimplify(Q; τ; P; σ) 13: if unsat = true Ω = then ψ true else ψ q Q τ q(q) ω Ω ω end if 14: end for 15: P, σ, unsat OrSimplify(P; σ) 16: if unsat = true then return true end if 17: Φ {σ p (p) p P, σ : P p σ p OP} 18: F ϕ Φ ϕ ψ Ψ ψ 19: else if F = ϕ Φ ϕ ψ Ψ ψ (ϕ:, ψ: ) then 20: /* ψ ψ = χ X χ ω Ω ω (χ:, ω: ). */ 21: Φ Φ, Ψ Ψ 22: if Ψ then 23: ψ Ψ ψ ExtendedWhite-Box( ψ Ψ ψ) 24: /* ψ ψ = χ X χ ω Ω ω (χ :, ω : ) ψ Ψ ψ ψ Ψ ψ. */ 25: if ψ Ψ ψ : then Φ Φ { ψ Ψ ψ }, Ψ end if 26: end if 27: for all ψ Ψ do 28: /* P PP(x 1,..., x n ) σ: P p σ p OP p P σ p (p) = ϕ Φ ϕ. */ 29: /* Q PP(x 1,..., x n ) τ: Q q τ q OP q Q τ q (q) = χ X χ. */ 30: Q, τ, unsat OrNestedSimplify(Q; τ; P; σ) 31: if unsat = true Ω = then ψ false else ψ q Q τ q(q) ω Ω ω end if 32: end for 33: P, σ, unsat AndSimplify(P; σ) 34: if unsat = true then return false end if 35: Φ {σ p (p) p P, σ : P p σ p OP} 36: F ϕ Φ ϕ ψ Ψ ψ 37: end if 38: return F 12

13 OS CPU: Intel Core i5-4300u 1.90GHz RAM: 8GB OS: Windows 8.1 Pro : VMware Player OS RAM: 4GB OS: Linux SMP 4.1 1: QE 207 QE, QE White-Box QE QE White-Box ( White-Box + QE) CAD QE,., 2., 3600 (1 ) ( A ), QE. 8. T 1 T 2 T 1 T 2 T 2 /T ( ) 1., T 1, T 2 QE White-Box QE ( ), QE White-Box ( White-Box + QE) ( ). 2.,. T 1 T 2,, 6 2. A White-Box,, false, White-Box. QE T 2 /T 1.,. ( 1, 3, 4, 5, 8) 13

14 4.2 2:,,. A. White-Box QE. 1 8 White-Box QE, White-Box. Redlog, SyNRAC, White-Box. QEPCAD 8, QEPCAD White-Box,. White-Box, QEPCAD 9 ( A ). White-Box,,., QEPCAD, QEPCAD, CAD [2].. 9 QEPCAD. 5, White-Box,. White-Box,,, QE., QE, Redlog, SyNRAC, White-Box., QEPCAD, White-Box.. 1, White-Box 4 (AndSimplify, OrSimplify, OrNestedSimplify, AndNestedSimplify). 2,, 1 White-Box. x + 1 > 0 y + 1 > 0 x + y + 2 > 0, x + 1 > 0, y + 1 > 0 x + y + 2 > 0,. A : 1 x 1 ((x 2 < 0 2x1 2 2x 1 1 0) (x 2 < 0 2x x 1 1 0) ( x1 2 x 1 1 x1 2 x 1 1) ( x1 2 + x 1 1 x1 2 + x 1 1) (2x1 2 2x 1 1 = 0 2x x 1 1 = 0) x 1 < 2 x 1 < 4 4x1 2 3 x2 1 x x1 2 + x x1 4 13x2 1 1 = 0) White-Box x 1 (0 < x 1 2 x 1 < 4 0 4x x4 1 13x2 1 1 = 0 2x2 1 2x 1 1 = 0 (x 2 < 0 2x1 2 2x 1 1 0)) Redlog x 1 (x 1 4 < 0 x 1 2 > 0 x1 2 x > 0 4x x4 1 13x2 1 1 = 0 (x 2 < 0 2x1 2 2x 1 1 0) (x 2 < 0 2x x 1 1 0) (2x1 2 2x 1 1 = 0 2x x 1 1 = 0)) 14

15 QEPCAD false SyNRAC 2 x 2 (( x x2 2 x2 1 x2 2 2)( x 2x 1 < 2 2x 2 2 x2 1 +x2 2 4x 2x 1 < 4)( x 2 x 1 < 2 x 4 2 8x3 2 x 1 8x 2 2 x2 1 8x2 2 < 16) (x 2 x 1 < 2 2x 2 2 x2 1 x2 2 4x 2x 1 < 4) (x 2 x 1 < 2 x x3 2 x 1 8x 2 2 x2 1 8x2 2 < 16) ( 6x2 2 x x x 4 2 x4 1 32x4 2 x2 1 +9x x2 2 x2 1 24x2 2 16)(6x2 2 x2 1 5x x4 2 x x4 2 x2 1 9x4 2 40x2 2 x x2 2 16) (6x2 2x2 1 3x x8 2 48x6 2 x x4 2 x4 1 48x x4 2 x x x2 2 x x )( 2x2 2x2 1 +x2 2 4x 2x 1 < 4 x2 4+8x3 2 x 1+8x2 2x2 1 +8x2 2 < 16)(2x2 2 x2 1 x2 2 4x 2x 1 < 4 x2 4 8x3 2 x 1+8x2 2x2 1 +8x2 2 < 16)( 48x 4 2 x x4 2 x2 1 19x4 2 56x2 2 x x x4 2 x x4 2 x x4 2 x x2 2 x4 1 9x x2 2 x x x )(24x4 2 x4 1 24x4 2 x2 1 +3x x2 2 x2 1 8x x8 2 48x6 2 x x4 2 x4 1 48x x4 2 x x x 2 2 x x ) (48x4 2 x4 1 64x4 2 x x x2 2 x2 1 32x x4 2 x x4 2 x4 1 90x4 2 x x 2 2 x x x2 2 x2 1 24x2 2 96x2 1 16) ( 6x2 2 x x2 2 < 4 24x4 2 x x4 2 x2 1 3x4 2 40x2 2 x x2 2 < 16 9x x6 2 x x4 2 x4 1 48x x4 2 x x x2 2 x x )(6x2 2 x2 1 3x2 2 < 4 24x4 2 x4 1 24x2 4x x x2 2 x2 1 8x2 2 < 16 9x8 2 48x6 2 x x4 2 x4 1 48x x4 2 x x x2 2 x x ) x 1 < 0 x 2 < 0 x2 2 2 x2 2 x2 1 + x x8 2 x x8 2 x x6 2 x x x6 2 x x4 2 x x x4 2 x x x2 2 x x = 0) White-Box Redlog false QEPCAD x 2 (x 2 > 0 x x 1 < 0 x 2 1 x2 2 x x4 1 x x4 1 x x4 1 x x2 1 x x2 1 x x 2 1 x x2 1 x x x x x = 0 (x2 2 2 = 0 x2 1 x2 2 x = 0) (x 1x > 0 2x 2 1 x x 1x 2 x > 0) (x 1x > 0 8x 2 1 x x 1x x x > 0) (2x2 1 x2 2 4x 1x 2 x < 0 8x 2 1 x2 2 8x 1x 3 2 +x4 2 +8x < 0)(2x2 1 x2 2 +4x 1x 2 x > 0 8x2 1 x2 2 +8x 1x 3 2 +x4 2 +8x < 0)(6x2 1 x2 2 5x x 4 1 x4 2 32x2 1 x x2 1 x2 2 +9x4 2 24x )(6x2 1 x2 2 5x x4 1 x4 2 32x2 1 x x2 1 x2 2 +9x4 2 24x ) (6x1 2x2 2 3x x4 1 x4 2 48x2 1 x x2 1 x x2 1 x x8 2 48x x x ) (6x1 2x2 2 3x < 0 24x4 1 x4 2 24x2 1 x x2 1 x x4 2 8x < 0 576x4 1 x4 2 48x2 1 x x2 1 x x 2 1 x2 2 +9x8 2 48x x x )(6x2 1 x2 2 3x > 0 24x4 1 x4 2 24x2 1 x x2 1 x2 2 +3x4 2 8x > 0 576x 4 1 x4 2 48x2 1 x x2 1 x x2 1 x2 2 +9x8 2 48x x x )(24x4 1 x4 2 24x2 1 x x2 1 x2 2 +3x4 2 8x x4 1 x4 2 48x2 1 x x2 1 x x2 1 x2 2 +9x8 2 48x x x )(48x4 1 x4 2 64x2 1 x x 2 1 x x4 2 32x x6 1 x x4 1 x x4 1 x x2 1 x x2 1 x x2 1 9x x )(48x4 1 x4 2 64x1 2x x2 1 x x4 2 32x x6 1 x x4 1 x x4 1 x x2 1 x x2 1 x x2 1 9x x )) false SyNRAC x 2 (( x x2 2 x2 1 x2 2 2)( x 2x 1 < 2 2x 2 2 x2 1 +x2 2 4x 2x 1 < 4)( x 2 x 1 < 2 x 4 2 8x3 2 x 1 8x 2 2 x2 1 8x2 2 < 16) (x 2 x 1 < 2 2x 2 2 x2 1 x2 2 4x 2x 1 < 4) (x 2 x 1 < 2 x x3 2 x 1 8x 2 2 x2 1 8x2 2 < 16) (9x4 1 6x x x ) ( 6x2 2 x x x4 2 x4 1 32x4 2 x x x2 2 x2 1 24x2 2 16) (6x2 2 x2 1 5x x 4 2 x x4 2 x2 1 9x4 2 40x2 2 x x2 2 16) ( 2x2 2 x2 1 + x2 2 4x 2x 1 < 4 x x3 2 x 1 + 8x 2 2 x x2 2 < 16)(2x 2 2 x2 1 x2 2 4x 2x 1 < 4 x 4 2 8x3 2 x 1 +8x 2 2 x2 1 +8x2 2 < 16)( 48x4 2 x x4 2 x2 1 19x4 2 56x2 2 x x x 4 2 x x4 2 x x4 2 x x2 2 x4 1 9x x2 2 x x x2 1 16)(48x4 2 x4 1 64x4 2 x x x2 2 x2 1 32x2 2 15

16 x 4 2 x x4 2 x4 1 90x4 2 x x2 2 x4 1 +9x x2 2 x2 1 24x2 2 96x2 1 16)( 6x2 2 x2 1 +3x2 2 < 4 24x4 2 x x2 4x2 1 3x4 2 40x2 2 x x2 2 < 16 9x8 2 48x6 2 x x4 2 x4 1 48x x4 2 x x x2 2 x x )(6x2 2x2 1 3x2 2 < 4 24x4 2 x4 1 24x4 2 x2 1 +3x x2 2 x2 1 8x2 2 < 16 9x8 2 48x6 2 x x4 2 x4 1 48x x4 2 x x x2 2 x x ) ( 64512x x x2 2 x x x x x2 2x x x2 2 x x x x x4 2 x2 1 +9x x2 2 x x4 1 24x x x x x2 2 x x x x ) x 1 < 0 x 2 < 0 x x2 2 x2 1 + x x 8 2 x x8 2 x x6 2 x x x6 2 x x4 2 x x x4 2 x x x2 2 x2 1 76x = 0) x 1 x 2 ( x 2 < 0 x 1 < 1 x x2 2 1 x2 1 x2 2 + x 1 0 x 2 1 x x 1 + 2x 2 1)) White-Box Redlog QEPCAD x 1 x 2 (0 < x 2 x 1 < 1 x x x2 1 + x2 2 2x 1 2x 2 + 1) x 1 x 2 (x 2 > 0 x < 0 x x x2 1 2x 1 + x 2 2 2x ) false SyNRAC 4 x 2 (x 2 < 0 x 1 + x 2 < 0 2x 1 x 2 + x x 1x 2 + x 2 2 < 1 x2 1 x 1x 2 + x 2 2 < 1 2x2 1 2x 1x 2 + 3x x x7 1 x x 6 1 x2 2 72x5 1 x x4 1 x4 2 72x3 1 x x2 1 x6 2 36x 1x x x6 1 24x5 1 x x 4 1 x2 2 96x 3 1 x x2 1 x x 1x x6 2 5x4 1 24x3 1 x x 2 1 x x 1x x x2 1 36x 1x x 2 2 < 9)) White-Box Redlog QEPCAD x 2 (x 2 < 0 0 < x 1 x 2 2x 2 1 2x 1x 2 + 3x x8 1 36x7 1 x x 6 1 x2 2 72x5 1 x x4 1 x4 2 72x3 1 x x 2 1 x6 2 36x 1x x x6 1 24x5 1 x x 4 1 x2 2 96x3 1 x x2 1 x x 1x x6 2 5x4 1 24x3 1 x x 2 1 x x 1 x x x2 1 36x 1x x 2 2 < 9) false SyNRAC 5 x 2 (x 2 < 2 x 2 2 x 1 0 4x x 1 2x 2 < 0 x x 1 4x 2 < 8 5x 2 2 4x 1 + 4x 2 4) White-Box Redlog false QEPCAD 16

17 false SyNRAC 6 x 4 ( x 4 < 0 x2 2x x 1x 2 x 3 + x2 2x 4 + x x 1x 4 0 x2 2x x 1x 2 x x2 2 x2 3 x 4 + x1 2x x 1x 2 x 3 x 4 2x 1 x3 2x 4 + 2x1 2x 4 < 0 x2 2x2 3 4x 2x x x 1x 2 x 3 4x 1 x3 2 + x2 2 x 4 4x 2 x 3 x 4 + 4x3 2x 4 + x1 2 2x 1x 4 0 x2 2x x 2x 5 3 x6 3 2x 1x 2 x x 1x3 4 x2 2 x2 3 x 4 + 2x 2 x 3 3 x 4 x3 4x 4 x1 2x2 3 4x 1x 2 x 3 x 4 + 4x 1 x3 2x 4 2x1 2x 4 < 0 x2 2x4 3 2x 2x x x 1x 2 x 3 3 2x 1x3 4 + x2 2 x2 3 x 4 2x 2 x 3 3 x 4 + 2x3 4x 4 + x1 2x x 1x 2 x 3 x 4 4x 1 x3 2x 4 + 2x1 2x 4 < 0 x2 4x4 3 +4x3 2 x5 3 8x2 2 x6 3 +8x 2x3 7 4x8 3 4x 1x 3 2 x x 1x2 2x4 3 16x 1x 2 x x 1x 6 3 2x4 2 x2 3 x 4 +8x 3 2 x3 3 x 4 16x2 2x4 3 x x 2 x 5 3 x 4 8x 6 3 x 4 6x1 2x2 2 x x2 1 x 2x 3 3 8x2 1 x4 3 4x 1x 3 2 x 3x 4 +12x 1 x2 2x2 3 x 4 24x 1 x 2 x 3 3 x 4+16x 1 x3 4x 4 x2 4x2 4 +4x3 2 x 3x4 2 8x2 2x2 3 x2 4 +8x 2x 3 3 x2 4 4x4 3 x2 4 4x3 1 x 2x 3 +4x 3 1 x2 3 2x2 1 x2 2 x 4+4x1 2x 2x 3 x 4 8x1 2x2 3 x 4 8x 1 x 2 x 3 x4 2+8x 1x3 2x2 4 x4 1 4x2 1 x2 4 0) White-Box false Redlog QEPCAD false SyNRAC 7 x 2 ((3x x x2 2 x 1 0) (15x2 2 x x x 1 0) (7x2 2 16x 2 5x 1 < 0 25x x x 1 < 64) (7x2 2 16x 2 5x 1 < 0 15x x2 2 5x 2x 1 40x 1 < 0) ( 5x x 2 + 3x 1 < 5 9x x x4 2 x x 3 2 x x2 2x x 2x x3 1 < 0) (5x2 2 10x 2 3x 1 < 5 198x x x3 2 x x2 2x x 2 x x2 1 < 0) (25x2 2 80x 2 15x 1 < 64 15x x2 2 5x 2x 1 40x 1 < 0) ( 198x x x3 2 x x2 2x x 2 x x2 1 < 0 9x x x4 2 x x 3 2 x x2 2x x 2x x3 1 < 0) ( 25x x x2 2 x 1 180x2 2 60x 2x 1 9x x x 1 < x x x5 2 x 1 216x x4 2 x x 3 2 x x3 2 x 1 375x2 2x x 2x x 2x x3 1 < 0) (25x x3 2 30x2 2 x x x 2x 1 + 9x x 2 12x 1 < x x x6 2 x 1 216x x5 2 x x2 4x x4 2 x x 3 2 x x2 2 x x2 2 x x 2x x x3 1 < 0)( 108x x x5 2 x 1 216x x4 2 x x 3 2 x x3 2 x 1 375x2 2x x 2x x 2x x3 1 < 0 135x x x6 2 x 1 216x x5 2 x x2 4x x4 2 x x 3 2 x x2 2 x x2 2 x x 2 x x x3 1 < 0)( 33x2 2 5x 1 < 0 3x2 2 +7x 1 < 0 15x2 2 x 1 0)( 3x2 2 7x 1 < 0 15x2 2 x x x 1 < 0) x 2 < 0 5x x 1 < 0 3x2 2 5x 1 < 0 x2 2 x 1 < 0 3x2 2 5x 1 < 0)) White-Box x 2 (0 < x 2 0 < 5x2 2 3x 1 x2 2 x 1 < 0(7x2 2 16x 2 5x 1 < 0 0 < 25x2 2 80x 2 15x 1 +64)(7x2 2 16x 2 5x 1 < 0 15x x2 2 5x 2x 1 40x 1 < 0)(0 < 5x2 2 10x 2 3x < 9x 6 2 9x x4 2 x 1 150x 3 2 x 1 25x2 2x x 2x1 2 25x 3 1 )(5x2 2 10x 2 3x 1 < 5 0 < 198x x x3 2 x 1 750x2 2x 1 250x 2 x x2 1 )(25x2 2 80x 2 15x 1 < 64 15x x2 2 5x 2x 1 40x 1 < 0) (0 < 198x x x3 2 x 1 750x2 2x 1 250x 2 x x2 1 0 < 9x 6 2 9x x4 2 x 1 150x 3 2 x 1 25x2 2x x 2x1 2 25x3 1 )(0 < 25x x3 2 30x2 2 x 1+180x2 2+60x 2x 1 +9x x 2 17

18 12x < 108x x x5 2 x x x4 2 x 1 300x 3 2 x x3 2 x x2 2x x 2x x 2x x 3 1 ) (25x x3 2 30x2 2 x x x 2x 1 + 9x x 2 12x 1 < 64 0 < 135x x x6 2 x x x5 2 x x2 4x x4 2 x x 3 2 x x2 2 x x2 2 x x 2x x x3 1 ) (0 < 108x x x5 2 x x x4 2 x 1 300x 3 2 x x3 2 x x2 2x x 2x x 2x x3 1 0 < 135x x x6 2 x x x5 2 x x2 4x x4 2 x x 3 2 x x2 2 x x2 2 x x 2 x x x3 1 )) Redlog QEPCAD 10x 2 13 > 0 3x 1 5x x 2 5 < 0 15x 1 25x x 2 64 > 0 x 1 x2 2 > 0 SyNRAC x 2 ((x 1 0 x2 2 0)(x x2 2 x 1 0)(7x2 2 16x 2 5x 1 < 0 25x x 2 +15x 1 < 64)(7x2 2 16x 2 5x 1 < 0 15x x2 2 5x 2x 1 40x 1 < 0) ( 5x x 2 + 3x 1 < 5 9x x x4 2 x x 3 2 x x2 2x x 2 x1 2+25x3 1 < 0)(5x2 2 10x 2 3x 1 < 5 198x x x3 2 x 1+750x2 2x 1+250x 2 x x2 1 < 0)(25x2 2 80x 2 15x 1 < 64 15x x2 2 5x 2x 1 40x 1 < 0)( 198x x x3 2 x x2 2x x 2 x x2 1 < 0 9x x x4 2 x x 3 2 x 1 +25x2 2x x 2x x3 1 < 0)( 25x x x2 2 x 1 180x2 2 60x 2x 1 9x x 2+12x 1 < x x x5 2 x 1 216x x4 2 x 1+300x 3 2 x x3 2 x 1 375x2 2x x 2x x 2 x x3 1 < 0) (25x x3 2 30x2 2 x x x 2x 1 + 9x x 2 12x 1 < x x x 6 2 x 1 216x x5 2 x x2 4x x4 2 x x 3 2 x x2 2 x x2 2 x x 2x x x3 1 < 0)( 108x x x5 2 x 1 216x x4 2 x x 3 2 x x3 2 x 1 375x2 2x x 2x x 2x x3 1 < 0 135x x x6 2 x 1 216x x5 2 x x2 4x x4 2 x x 3 2 x x2 2 x x2 2 x x 2 x x x3 1 < 0) x 2 < 0 5x x 1 < 0 3x2 2 5x 1 < 0 x2 2 x 1 < 0 3x2 2 5x 1 < 0) 8 x 1 ( x 1 < 0 x 1 1 x2 2 + x 1 < 14x x2 2 4x 2 + x 1 < 116x2 4 +8x3 2 16x2 2 x 1 15x x2 1 8x 2 + x 1 1 0) White-Box x 1 (0 < x 1 x2 2 + x 1 < 1 4x x2 2 4x 2 + x 1 < 1 16x x3 2 16x2 2 x 1 15x x2 1 8x 2 + x 1 1 0) Redlog QEPCAD x 1 (0 < x 1 x2 2 + x 1 < 1 4x x2 2 4x 2 + x 1 < 1 16x x3 2 16x2 2 x 1 15x x2 1 8x 2 + x 1 1 0) SyNRAC 9 x 1 > 0 x 30 > 0 x x 30 > 0 White-Box x 1 > 0 x 30 > 0 ( ) Redlog x 1 > 0 x 30 > 0 ( ) QEPCAD 18

19 SyNRAC time out ( 3600 ) ( ) [1],. QE., [2] C. W. Brown. QEPCAD B: A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin, 37(4), pp , [3] C. W. Brown. Fast simplifications for Tarski formulas based on monomial inequalities. J. Symbolic Comput, 47, pp , [4] C. W. Brown and A. Strzeboński. Black-Box/White-Box Simplification and Applications to Quantifier Elimination. Proc. ISSAC, ACM, pp , [5] B. F. Caviness and J. R. Johnson (Eds.). Quantifier Elimination and Cylindrical Algebraic Decomposition (Texts and Monographs in Symbolic Computation), Springer, [6] D. Cox, J, Little, D. O Shea. Ideals, Varieties, and Algorithms An Introduction to Computational Algebraic Geometry and Commutative Algebra (Third Edition), Springer, [7] A. Dolzmann, T. Sturm. Redlog [Computer software], /01/14. [8]. SyNRAC [Computer software], /12/04. [9] Hoon Hong, C. W. Brown. QEPCAD B [Computer software], QEPCAD.html, 2016/01/14. [10] R. Loos and V. Weispfenning. Applying linear quantifier elimination, The Computer Journal, 36(5), pp , [11] Maple, a division of Waterloo Maple Inc. Maple 18 [Computer software], Waterloo, Ontario, Canada. [12] T. Strum and A. Dolzmann. Simplification of quantifier-free formulae over ordered fields, J. Symbolic Comput, 24, pp ,