c++ - C++ で DPLL を最適に実装する方法は?

Question

C++ でDPLLアルゴリズムを実装しようとしていますが、このタイプの再帰問題を解決するにはどのようなデータ構造が最適か疑問に思っています。現在、ベクターを使用していますが、コードが長くて見にくいです。何か提案はありますか？

function DPLL(Φ)
   if Φ is a consistent set of literals
       then return true;
   if Φ contains an empty clause
       then return false;
   for every unit clause l in Φ
      Φ ← unit-propagate(l, Φ);
   for every literal l that occurs pure in Φ
      Φ ← pure-literal-assign(l, Φ);
   l ← choose-literal(Φ);
   return DPLL(ΦΛl) or DPLL(ΦΛnot(l));

Answer 1

配列は、任意の命題へのランダム アクセスを提供するため、現在の割り当てを表すのに適しています。節を表すために、命題インデックスの STL のセットを使用できます。

非常に効率的な SAT ソルバーを実装するには、さらにデータ構造が必要になります (監視対象のリテラルと説明を格納するため)。これらの概念の非常に読みやすい紹介は、http://poincare.matf.bg.ac.rs/~filip/phd/sat-tutorial.pdfにあります。