exactly
n SAT の前につけて、任意の節が丁度 n 個のリテラルを持つように制限する
n SAT は任意の節が高々 n 個のリテラルを持つように制限している
exactly条件の下で変数のみの節を組み合わせることで実質定数を作成できれば、実質定数を節に組み込むことで非 exactly n SAT から帰着できる。