3 角形の辺の長さと C.A.D.

前回の benchmark における変数順序，a, b, c についての不等式制約，各問題の処理時間とそれらの合計（ms）は，次の通りです．

[m, a, b, c]
a<b+c, b<c+a, c<a+b
[117,115,208,1341,169,365,463,1661,233,947,2188,1301,579,395,216,743,751,101,456,1198,432]
13979

この不等式制約では，各式に a, b, c の全てが現れるため，それらの値を与えるまで各式の真偽は定まりませんが，C.A.D. の lifting phase では下位から上位へと cell を構成するため，より早い（低い）段階で真偽が定まる式を制約に含めることで，不要な cell の生成が減り，処理時間の短縮が望めます．

実際，a＜b+c, b＜c+a, c＜a+b から直ちに導かれ，一見過剰に思える 0＜a, 0＜b, 0＜c のうち，下位の変数からなる 2 つを制約に加えると

[m, c, b, a] 0<c, 0<b, a<b+c, b<c+a, c<a+b (No.18,21)
[m, a, b, c] 0<a, 0<b, a<b+c, b<c+a, c<a+b (otherwise)
[154,138,285,555,138,304,380,624,181,422,762,652,215,357,164,336,328,85,297,493,191]
7061

のように高速化します．また，問題の対称性に従い，定義域を制限しても値域は不変なので，変数の大小関係を制約に加えると

[m, c, b, a] 0<c, c<=b, a<b+c, b<c+a (No.18,21)
[m, a, b, c] 0<a, a<=b,, b<c+a c<a+b (otherwise)
[151,124,218,416,117,247,379,507,169,372,507,457,197,276,151,262,259,80,216,317,142]
5564

更に，目標が同次式の比の値であることから，何れかひとつの変数を 1 としても値域は不変なので，最下位の変数を 1 とすると

[m, b, a] 1<=b, a<b+1, b<1+a (No.18,21)
[m, b, c] 1<=b, b<c+1, c<1+b (otherwise)
[119,88,106,195,125,148,184,259,107,175,411,295,144,158,108,161,162,54,87,219,100]
3405

同じく，全ての変数に関して対称な問題で，1=a<=b<=c とすると

[m, b, a] 1<=b, a<b+1, b<1+a (No.18,21)
[m, b, c] 1<=b, b<c+1, c<1+b (No.1, 2)
[m, b, c] 1<=b, b<=c, c<1+b (otherwise)
[113,86,107,200,117,158,204,236,121,227,365,291,210,140,118,158,179,54,95,205,109]
3493

といった結果を得ます．