2-SATを探索で解く方法とyukicoder No.470 Inverse S+T Problem

2-SATを想定解とする問題をyukicoderで出題しました。
No.470 Inverse S+T Problem - yukicoder

想定解通りの2-SAT解法とは別に、計算量のよく分からない探索を結構通されてしまいました。
探索解の中に正当なものがあるのか、調べていたところ2-SATを暗黙的に解いている提出が見つかりました。
たとえばヘクトさんの提出です。

その解き方というのが、Wikipediaの2-SATの解法の一つとして載っているLimited backtrakingです。
2-satisfiability - Wikipedia
http://epubs.siam.org/doi/abs/10.1137/0205048

例を用いて大雑把に説明します。
$(\lnot x_1 \lor x_2) \land (\lnot x_1 \lor \lnot x_2) \land (\lnot x_1 \lor x_5) \land (x_1 \lor x_3) \land (\lnot x_3 \lor x_4) \land (x_5 \lor x_6)$
が充足可能か調べましょう。

真であると分かったリテラルの集合を $T$ で表します。
まず適当な変数を選び( $x_1$ とします)真だと仮定します。( $T = \{ x_1 \}$ )
$\lnot x_1$ は偽になるので、このリテラルを含む節では、もう片方が真になる必要があります。
1つめの節から $T$ に $x_2$ を加えます。
2つめの節から $T$ に $\lnot x_2$ を加えます。
ここで $T = \{ x_1, x_2, \lnot x_2 \}$ となり、矛盾が見つかりました。

今度は $x_1$ が偽だと仮定します。( $T = \{ \lnot x_1 \}$ )
$x_1$ を含む節に注目します。
4つめの節から $T$ に $x_3$ を加えます。
$x_1$ を含む節は1つだけです。新たに $T$ に加わった $x_3$ に対して、 $\lnot x_3$ を含み、真であることが確定していない節に注目します。
5つめの節から $T$ に $x_4$ を加えます。
これで( $T = \{ \lnot x_1, x_3, x_4\}$ )になりました。これ以上 $T$ に追加することもできませんし、矛盾もみつかりませんでした。