DPLL_Presentation_Russian

1.

Алгоритм DPLL (Davis-PutnamLogemann-Loveland)
Минимум текста, больше
наглядности

2.

Этапы алгоритма DPLL
• Основные этапы:
• - Unit Propagation
• - Pure Literal Elimination
• - Рекурсивное ветвление

3.

1. Unit Propagation (Пропаганда
одиночных литеров)
• Определение значений для одиночных
переменных для упрощения формулы.

4.

2. Pure Literal Elimination
• Удаление переменных, которые имеют
одно значение, чтобы сократить
выражение.

5.

3. Рекурсивное ветвление
• Попытка назначения значений переменным
для проверки выражения.

6.

Наглядный пример
• Пример: (x ∨ y) ∧ (¬x ∨ z) ∧ (¬z)

7.

Пример на Python
• Пример кода Python для DPLL,
иллюстрирующий пошаговое выполнение
алгоритма.