Обсуждение:DPLL

Последнее сообщение: 25 дней назад от Safaesr в теме «Сценарии использования»

Сценарии использования править

Мне непонятно, для чего этот алгоритм нужен. Ну решает он задачу SAT, я даже, наверное, смогу его запрограммировать, и будет он мне для булевой формулы подбирать какие-то значения переменных, при которых формула станет истинной. И что? Неясно, как это всё связывается с доказательствами корректности, или с доказательствами теорем. Safaesr (обс.) 17:07, 25 апреля 2024 (UTC)Ответить