P vs NP 問題の結論などどうでもよくなった？

計算機科学の世界では有名な問題のひとつに「P vs NP 問題」と呼ばれるものがあるが，この問題の結論などどうでもよくなってしまう画期的な計算機が開発されたらしい．ちなみにその計算機は「ネ申（ねしん）」という名前なのだそうな．

一例として，有名な NP 困難の問題のひとつである充足可能性問題を取り上げよう．この問題を解く C 言語のプログラム（の一部分）を，普通の計算機向けに書けば次のようになるだろう．少々ひねくれたコードに見えるかもしれないが，説明の都合によるものなので気にしないでいただきたい．

/**
 *  Solves the satisfiability problem.
 *
 *  @param f  the target boolean formula
 *  @param x  the array to contain an assaignment
 *  @param n  the number of variables
 */
bool solve_sat
(Formula f, bool x[], int n)
{
    return solve_sat_core( f, x, 0, n, true  ) ||
           solve_sat_core( f, x, 0, n, false ) ;
}

bool solve_sat_core
(Formula f, bool x[], int i, int n, bool xi)
{
    x[i] = xi;

    if(i == n - 1) {
        return evaluate(f, x, n);
    }
    else {
        return solve_sat_core( f, x, i + 1, n, true  ) ||
               solve_sat_core( f, x, i + 1, n, false ) ;
    }
}

このプログラムは，変数がひとつ増えるごとに，計算時間がだいたい倍になる．別の表現をすれば，このプログラムにおける時間計算量は O(2^n) である．

ところで，「ネ申」向けに開発されたコンパイラには独自拡張の演算子として ||| というものが用意されている．これは論理和を計算する演算子だが，以下に記すような大変特徴的な挙動をしめす．

2 個のオペランドのうち，結果が真になるものだけを評価する．
両者とも真になるときはどちらかだけを評価する．
両者とも偽になるときはどちらも評価しない．

「ネ申」には godjz という特別な機械語命令が実装されているらしい．この機械語命令は，現在番地から指定番地までを実行したとき，アキュムレータが零になるか非零になるかを（一瞬のうちに）判定して，零になるときは指定番地にジャンプする．先の演算子はコンパイラによってこの演算子の呼び出しに翻訳される．模式的に書くとこんな感じだろうか．

        godjz   $1
        call    solve_sat_core         ;; the result is set to accumulator
$1:     jnz     $2
        godjz   $2
        call    solve_sat_core         ;; the result is set to accumulator
$2:     ...

勘のいい人ならば，既に気づいたことと思うが，先ほどの充足可能性問題のプログラムにおいて，普通の演算子 || のところを魔法の演算子 ||| に置き換えるだけで，どんな式に対しても変数の数について線形時間（あるいは論理式の長さについて線形時間かもしれない）で問題を解くプログラムに変えることができる．

このように，「ネ申」は充足可能性問題を変数の数について線形時間で解くことができる．すなわち，「ネ申」さえあれば全ての（計算可能な）判定問題が多項式時間で解けるということになる．