Как лучше всего реализовать 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.