dnf から cnf へ

式の簡約は，まず選言形に直し，得られた連言項毎に処理するのが基本です．よって結果は

(%i70) qe([],(a^2=1)%and(b^2=1));
Evaluation took 0.3400 seconds (0.5200 elapsed) using 12.210 MB.
(%o70) (a-1 <= 0) %and (a+1 >= 0)
                  %and (((a-1 = 0) %and (b-1 = 0))
                   %or ((a-1 = 0) %and (b+1 = 0))
                   %or ((a+1 = 0) %and (b-1 = 0))
                   %or ((a+1 = 0) %and (b+1 = 0))) %and (b-1 <= 0)
                  %and (b+1 >= 0)
(%i71) nns(%);
Evaluation took 4.5500 seconds (5.5200 elapsed) using 185.040 MB.
(%o71) ((a-1 = 0) %and (b-1 = 0)) %or ((a-1 = 0) %and (b+1 = 0))
                                  %or ((a+1 = 0) %and (b-1 = 0))
                                  %or ((a+1 = 0) %and (b+1 = 0))

のようになります．これは連立方程式の解の表示として標準的ですが，連言形のほうが見易そうです．実際

(%i72) cnf(%);
Evaluation took 0.2900 seconds (0.3300 elapsed) using 9.648 MB.
(%o72) ((a-1 = 0) %or (a+1 = 0)) %and ((a-1 = 0) %or (a+1 = 0) %or (b-1 = 0))
                                 %and ((a-1 = 0) %or (a+1 = 0) %or (b-1 = 0)
                                                 %or (b+1 = 0))
                                 %and ((a-1 = 0) %or (a+1 = 0) %or (b+1 = 0))
                                 %and ((a-1 = 0) %or (b-1 = 0) %or (b+1 = 0))
                                 %and ((a+1 = 0) %or (b-1 = 0) %or (b+1 = 0))
                                 %and ((b-1 = 0) %or (b+1 = 0))
(%i73) nns(%);
Evaluation took 3.9800 seconds (5.3500 elapsed) using 177.244 MB.
(%o73) ((a-1 = 0) %or (a+1 = 0)) %and ((b-1 = 0) %or (b+1 = 0))

といった具合です．勿論，初めからこの結果を目指して

(%i74) map(nnsolve,(a^2=1)%and(b^2=1));
Evaluation took 0.0100 seconds (0.0100 elapsed) using 494.719 KB.
(%o74) ((a = -1) %or (a = 1)) %and ((b = -1) %or (b = 1))

とすることも出来ます．