Posted at

C++11TMPでコンパイル時にSATを解く

More than 1 year has passed since last update.

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を解くことに利用した形になります。


コード理解のヒント


Parity SATをコンパイル時に解く

上記コードでは、オーバーロード解決の優先順位をつけていましたが、これをつけないと変数への真偽値割り当てがどちらでもSatisfiableにできる場合に、オーバーロード解決があいまいになってしまいます。オーバーロード解決があいまいになることは、SFINAEの対象です。

どういう時にオーバーロード解決が成功するかを考えると、「部分問題の解が2つある」と「部分問題の解が存在しない」のどちらもSFINAEになることから、mod 2の世界で考えればいいとわかります。つまり、全体の解が奇数個存在するときのみオーバーロード解決が成功すると言えます。

ところで、「SATの解の個数が奇数個であるか?」という問題をParity SATと言いますが、完全にこれの定義に合致します。よって、先のコードでオーバーロード解決の優先順位をつけていたところをなくす(longintに書き換える)だけでParity SATを解くことができます!

(「SATの解が唯一であるか?」という問題を解いているわけではない点には注意が必要です)

実行結果→[Wandbox]三へ( へ՞ਊ ՞)へ ハッハッ


注意

SATソルバーのようにかしこい方法を使って解くわけではなく、枝刈りなしのバックトラックを行いすべてのパスでテンプレートをインスタンス化するため、13変数でGBオーダーのメモリーを使います。

また、なぜかUnsatisfiableなパスの方が多くメモリを消費するため、そういったパスが多いとclangが落ちてしまうことがあります。