DPLLアルゴリズム
再帰呼び出しを用いたDPLLアルゴリズムの疑似コードは以下のように表現できる。 節集合 F が入力で、結果は"充足可能"、"充足不能"のいずれかである。
実際のプログラムでは、以下の変更が加えられることがある。
純リテラル規則は省略されることが多い。チェックのために手間がかかり十分な効果が得にくいため。
分割規則を適用する原子論理式 v と最初にチェックする真理値 b の選択には、何らかのヒューリスティックを用いる。
再帰呼び出しを繰り返しに変え、バックトラックは明示的に行う。
(1レベル以上のバックトラックにより効率化を行える場合がある)
手続き内での情報は学習などにより再利用する。