Существует множество проблем и решателей SAT.
Я вижу и использую множество автономных и онлайновых решателей SAT для сравнения и анализа различных экземпляров. Для любопытства я хочу протестировать различные алгоритмы, описанные в статьях для kSAT.
Как реализовать решатель SAT, такой как решатели на основе DPLL, python, c ++ или другими? Я очень заинтересован в этом.
Формат ввода может быть DIMACS-CNF, например
1 -5 4 0
-1 5 3 4 0
представляет формулу (x1 ∨ ¬x5 ∨ x4) ∧ (¬x1 ∨ x5 ∨ x3 ∨ x4).