ncond 動かない式を動かす

以前にも述べましたが，変数の個数を低減させた必要条件を付加する ncond は強力で，nnss，nnsolvexx の求解能力はこの関数によるヒントの賜物とも言えます．

(%i98) f:(a^2+b^2+c^2<=3)%and(a*b*c>=1)$
Evaluation took 0.0100 seconds (0.0200 elapsed) using 538.359 KB.
(%i99) qe([],f);
Evaluation took 0.3500 seconds (0.5500 elapsed) using 17.918 MB.
(%o99) (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (a*b*c-1 = 0)
(%i100) nnss(f);
Evaluation took 17.1500 seconds (23.0500 elapsed) using 952.370 MB.
(%o100) ((a-1 = 0) %and (b-1 = 0) %and (c-1 = 0))
  %or ((a-1 = 0) %and (b+1 = 0) %and (c+1 = 0))
  %or ((a+1 = 0) %and (b-1 = 0) %and (c+1 = 0))
  %or ((a+1 = 0) %and (b+1 = 0) %and (c-1 = 0))

verbose モード．

(%i101) prt(x):=print(x)$
Evaluation took 0.0000 seconds (0.0000 elapsed) using 200 bytes.
(%i102) nnss(f);

pre-simplified formula 
2 
(a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (a*b*c-1 = 0) 
necessary condition 
a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0 
a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0 
b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0 
((a-1 = 0) %and (a-1 <= 0) %and (a+1 >= 0))
  %or ((a-1 <= 0) %and (a+1 = 0) %and (a+1 >= 0))
  
((b-1 = 0) %and (b-1 <= 0) %and (b+1 >= 0))
  %or ((b-1 <= 0) %and (b+1 = 0) %and (b+1 >= 0))
  
((c-1 = 0) %and (c-1 <= 0) %and (c+1 >= 0))
  %or ((c-1 <= 0) %and (c+1 = 0) %and (c+1 >= 0))
  
true 
8 
((a-1 = 0) %and (a-1 <= 0) %and (a+1 >= 0) %and (b-1 = 0) %and (b-1 <= 0)
           %and (b+1 >= 0) %and (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0)
           %and (c-1 = 0) %and (c-1 <= 0) %and (c+1 >= 0) %and (a*b*c-1 = 0)
           %and (a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0)
           %and (b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0))
  %or ((a-1 = 0) %and (a-1 <= 0) %and (a+1 >= 0) %and (b-1 = 0)
                 %and (b-1 <= 0) %and (b+1 >= 0)
                 %and (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (c-1 <= 0)
                 %and (c+1 = 0) %and (c+1 >= 0) %and (a*b*c-1 = 0)
                 %and (a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0)
                 %and (b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0))
  %or ((a-1 = 0) %and (a-1 <= 0) %and (a+1 >= 0) %and (b-1 <= 0)
                 %and (b+1 = 0) %and (b+1 >= 0)
                 %and (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (c-1 = 0)
                 %and (c-1 <= 0) %and (c+1 >= 0) %and (a*b*c-1 = 0)
                 %and (a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0)
                 %and (b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0))
  %or ((a-1 = 0) %and (a-1 <= 0) %and (a+1 >= 0) %and (b-1 <= 0)
                 %and (b+1 = 0) %and (b+1 >= 0)
                 %and (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (c-1 <= 0)
                 %and (c+1 = 0) %and (c+1 >= 0) %and (a*b*c-1 = 0)
                 %and (a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0)
                 %and (b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0))
  %or ((a-1 <= 0) %and (a+1 = 0) %and (a+1 >= 0) %and (b-1 = 0)
                  %and (b-1 <= 0) %and (b+1 >= 0)
                  %and (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (c-1 = 0)
                  %and (c-1 <= 0) %and (c+1 >= 0) %and (a*b*c-1 = 0)
                  %and (a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0)
                  %and (b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0))
  %or ((a-1 <= 0) %and (a+1 = 0) %and (a+1 >= 0) %and (b-1 = 0)
                  %and (b-1 <= 0) %and (b+1 >= 0)
                  %and (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (c-1 <= 0)
                  %and (c+1 = 0) %and (c+1 >= 0) %and (a*b*c-1 = 0)
                  %and (a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0)
                  %and (b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0))
  %or ((a-1 <= 0) %and (a+1 = 0) %and (a+1 >= 0) %and (b-1 <= 0)
                  %and (b+1 = 0) %and (b+1 >= 0)
                  %and (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (c-1 = 0)
                  %and (c-1 <= 0) %and (c+1 >= 0) %and (a*b*c-1 = 0)
                  %and (a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0)
                  %and (b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0))
  %or ((a-1 <= 0) %and (a+1 = 0) %and (a+1 >= 0) %and (b-1 <= 0)
                  %and (b+1 = 0) %and (b+1 >= 0)
                  %and (a^2*b^4+a^4*b^2-3*a^2*b^2+1 = 0) %and (c-1 <= 0)
                  %and (c+1 = 0) %and (c+1 >= 0) %and (a*b*c-1 = 0)
                  %and (a^2*c^4+a^4*c^2-3*a^2*c^2+1 = 0)
                  %and (b^2*c^4+b^4*c^2-3*b^2*c^2+1 = 0))
  
simplifing... 
{(a-1 = 0) %and (b-1 = 0) %and (c-1 = 0),
 (a-1 = 0) %and (b+1 = 0) %and (c+1 = 0),
 (a+1 = 0) %and (b-1 = 0) %and (c+1 = 0)}
  
{(a-1 = 0) %and (b-1 = 0) %and (c-1 = 0),
 (a-1 = 0) %and (b+1 = 0) %and (c+1 = 0),
 (a+1 = 0) %and (b+1 = 0) %and (c-1 = 0)}
  
{(a-1 = 0) %and (b-1 = 0) %and (c-1 = 0),
 (a+1 = 0) %and (b-1 = 0) %and (c+1 = 0),
 (a+1 = 0) %and (b+1 = 0) %and (c-1 = 0)}
  
{(a-1 = 0) %and (b+1 = 0) %and (c+1 = 0),
 (a+1 = 0) %and (b-1 = 0) %and (c+1 = 0),
 (a+1 = 0) %and (b+1 = 0) %and (c-1 = 0)}
  
{a-1 = 0,b-1 = 0} 
{a-1 = 0,c-1 = 0} 
{b-1 = 0,c-1 = 0} 
{a-1 = 0,b+1 = 0} 
{a-1 = 0,c+1 = 0} 
{b+1 = 0,c+1 = 0} 
{a+1 = 0,b-1 = 0} 
{a+1 = 0,c+1 = 0} 
{b-1 = 0,c+1 = 0} 
{a+1 = 0,b+1 = 0} 
{a+1 = 0,c-1 = 0} 
{b+1 = 0,c-1 = 0} 
Evaluation took 18.5100 seconds (24.4700 elapsed) using 954.651 MB.
(%o102) ((a-1 = 0) %and (b-1 = 0) %and (c-1 = 0))
  %or ((a-1 = 0) %and (b+1 = 0) %and (c+1 = 0))
  %or ((a+1 = 0) %and (b-1 = 0) %and (c+1 = 0))
  %or ((a+1 = 0) %and (b+1 = 0) %and (c-1 = 0))