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が落ちてしまうことがあります。