CDCLSolver.deduce

単位伝播を繰り返します。 途中で矛盾が生じたら CONFLICT を返します。 矛盾なくすべての変数に真偽値を割り当てられたら SAT を返します。 それ以外の場合には OK を返します。