Возьмем следующий набор логических утверждений:
А: Б ложно
Б: С ложно
C: B или A верно
Мне дали задание формализовать это так, чтобы DPLL мог определить, есть ли решение (какие правила верны, какие ложны), не приводящее к противоречию.
Проблема в том, что я понятия не имею, как это сделать. Онлайн-решатели ожидают выражения в определенном формате, как здесь: http://www.inf.ufpr.br/dpasqualin/d3-dpll/
Как преобразовать мои утверждения в эти числа?
Возможно, вы путаете обозначения: я предполагаю, что здесь три оператора и три переменные. Я буду использовать строчные буквы для переменных и прописные буквы для операторов, чтобы было понятно:
Statement A: not b
Statement B: not c
Statement C: a or b
Теперь замените строчные буквы цифрами:
Statement A: not 2
Statement B: not 3
Statement C: 1 or 2
not следует записывать как отрицательный знак, а or заменять двоеточием. Полученные три строки теперь можно ввести в связанный с вами SAT-решатель:
-2
-3
1, 2
Он выводит 1, -2, -3 в качестве решения, поэтому переменная a должна быть истинной, а b и c — ложной.
