C++のテンプレートメタプログラミング(TMP)はチューリング完全ですので、当然 充足可能性問題(SAT)を解くこともできます。
コンパイル時に分岐するための技法としてSFINAEがありますが、これを使うと少ないコード量でコンパイル時にSATを解くコードを書くことができることに気づきました。
SATをコンパイル時に解くコード
template<bool...> struct Var {};
template<bool...> struct Satisfiable {};
struct Unsatisfiable {};
template<bool... Vs>
auto search( Var<Vs...> )
-> decltype( problem( Var<Vs...>{} ) );
template<bool... Vs, class... Rest>
auto search( Var<Vs...>, int, Rest... )
-> decltype( search( Var<Vs..., true>{}, Rest{}... ) );
template<bool... Vs, class... Rest>
auto search( Var<Vs...>, long, Rest... )
-> decltype( search( Var<Vs..., false>{}, Rest{}... ) );
template<class... Ts>
auto solve( Ts... ) -> decltype( search( Var<>{}, Ts{}... ) );
auto solve( ... ) -> Unsatisfiable;
# include <type_traits>
template<
bool V1, bool V2, bool V3, bool V4,
typename std::enable_if<
( V1 || V2 )
&& ( V1 || !V2 || V4 )
&& ( !V1 || !V2 || !V3 || !V4 )
, std::nullptr_t>::type = nullptr
>
auto problem( Var<V1, V2, V3, V4> )
-> Satisfiable<V1, V2, V3, V4>;
# include <iostream>
# include <typeinfo>
int main() {
decltype( solve( 0, 0, 0, 0 ) ) ans;
std::cout << typeid(ans).name() << std::endl;
}
$ clang++ -std=c++11 sat.cpp
$ ./a.out | c++filt -t
Satisfiable<true, true, true, false>
実行結果→[Wandbox]三へ( へ՞ਊ ՞)へ ﾊｯﾊｯ
オーバーロード解決が成功する、つまりSubstitutionが成功するかは、decltype内で呼び出されている関数のオーバーロード解決が成功するかに依存しています。深く呼び出した先の関数でSFINAEが起きた場合はバックトラックが起こるので、それをSATを解くことに利用した形になります。
コード理解のヒント
-
std::nullptr_tとnullptrを使ったSFINAE(参照: Qiita: std::enable_ifを使ってオーバーロードする時、enablerを使う？) -
search関数は、後ろに宣言されている関数を参照するが、同じ名前空間上にあるstruct Var<...>が引数に入っているためADLで検索されて問題なく参照できる - オーバーロード解決の優先順位をつけるために、
0というintを関数に渡し、オーバーロード解決の優先順位がint>longなことを利用する(参照：本の虫: C++11におけるモダンなhas_xxxの実装の追記解説)
Parity SATをコンパイル時に解く
上記コードでは、オーバーロード解決の優先順位をつけていましたが、これをつけないと変数への真偽値割り当てがどちらでもSatisfiableにできる場合に、オーバーロード解決があいまいになってしまいます。オーバーロード解決があいまいになることは、SFINAEの対象です。
どういう時にオーバーロード解決が成功するかを考えると、「部分問題の解が2つある」と「部分問題の解が存在しない」のどちらもSFINAEになることから、mod 2の世界で考えればいいとわかります。つまり、全体の解が奇数個存在するときのみオーバーロード解決が成功すると言えます。
ところで、「SATの解の個数が奇数個であるか？」という問題をParity SATと言いますが、完全にこれの定義に合致します。よって、先のコードでオーバーロード解決の優先順位をつけていたところをなくす(longをintに書き換える)だけでParity SATを解くことができます！
(「SATの解が唯一であるか？」という問題を解いているわけではない点には注意が必要です)
実行結果→[Wandbox]三へ( へ՞ਊ ՞)へ ﾊｯﾊｯ
注意
SATソルバーのようにかしこい方法を使って解くわけではなく、枝刈りなしのバックトラックを行いすべてのパスでテンプレートをインスタンス化するため、13変数でGBオーダーのメモリーを使います。
また、なぜかUnsatisfiableなパスの方が多くメモリを消費するため、そういったパスが多いとclangが落ちてしまうことがあります。