DPLLをC++に最適に実装する方法は？

Question

私はDPLLアルゴリズムをC++で実装しようとしていますが、この種の再帰問題を解決するにはどのような種類のデータ構造が最適だろうと思います。今はベクトルを使用していますが、コードは長くて醜いです。提案はありますか？

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です。