Рефал - определение равносильности логических формул

[DoGGy]

Приветствую обитателей данного форума. Давненько я сюда не зяглядывал :)
Вот не могу придумать как запрограммировать задачу определения равносильности логических формул на языке Рефал. Крутится пару мыслей чисто теоретических, привести формулы к СДНФ или полиному Жегалкина и сравнивать уже их, т.к. в случае равносильности они должны быть одинаковы. Но вот придумать алгоритм таких преобразований не получается. Может есть какие-то известные или готовые реализации, может даже и на Рефале (было бы вообще очень хорошо) ?
Буду благодарен любой помощи.

[Sonic86]

А это не NP-полная задача случаем?
Например, определить для булевых формул $F,G$ верно ли $F \leftrightarrow G$? При $G = 0$ получаем проблему выполнимости $F$ (т.е. определить, существуют ли $x_1,...,x_n : F(x_1,...,x_n) = 1$ или нет). А это уже NP-полная задача (англоязычно, кажется, $k$-SAT)
Я это к тому, что если NP-полная задача, то либо по сути перебор (а значит явный перебор вполне годится, а он прост), либо вам дают $10^6$ денег. Хотя может есть какие-то хорошо оптимизированные алгоритмы.

[Circiter]

Под явным перебором подразумевается сравнение таблиц истинности сопоставляемых формул?

[Sonic86]

Circiter в сообщении #505043 писал(а):

Под явным перебором подразумевается сравнение таблиц истинности сопоставляемых формул?

Да, например типа такого:

f=1;
for(x_1=0;1;x_1++){
for(x_2=0;1;x_2++){
...
for(x_n=0;1;x_n++){
if(F(x_1,...,x_n)!=G(x_1,...,x_n)){f=0;}
}
...
}
}
return f;

Конечно, $n$ параметр и надо на самом деле не так, но мне неохота вспоминать как надо

Если я что-то наврал, скажите сразу

Вообще задача выполнимости и задача ТС равносильны даже: эквивалентность двух формул равносильна невыполнимости $\neg (F \leftrightarrow G)$.

[Circiter]

2Sonic86

Цитата:

Если я что-то наврал, скажите сразу

В-принципе смысл улавливается. Только в качестве условия в цикле нужно использовать x<=1, а вместо f=0 достаточно сразу написать return 0, а в конце вернуть истину (на деле, елка из циклов здесь вообще не нужна, мы же фактически просто перебираем все двоичные числа с разрядностью в количество переменных). Да, сравнение таблиц истинности я примерно так себе и представлял, спасибо.

А вот вашу формулу $\neg(F\leftrightarrow G)$ в упор не понимаю. Если надо установить эквивалентность, то причем тут отрицание? :)

[Sonic86]

Circiter в сообщении #505295 писал(а):

Только в качестве условия в цикле нужно использовать x<=1

Угу, косяк, плохо писать сразу на нескольких языках

Circiter в сообщении #505295 писал(а):

а вместо f=0 достаточно сразу написать return 0, а в конце вернуть истину

Я не утверждал, что данный код оптимизирован.

Circiter в сообщении #505295 писал(а):

на деле, елка из циклов здесь вообще не нужна, мы же фактически просто перебираем все двоичные числа с разрядностью в количество переменных

Ну да, мне просто в лом было вспоминать, как двоичные числа перебираются, код бы стал больше...

Circiter в сообщении #505295 писал(а):

Да, сравнение таблиц истинности я примерно так себе и представлял, спасибо.

А! Ну значит хорошо Я просто думал, что у меня ошибка.

Circiter в сообщении #505295 писал(а):

А вот вашу формулу $\neg(F\leftrightarrow G)$ в упор не понимаю. Если надо установить эквивалентность, то причем тут отрицание? :)

Я не помню точной формулировки задачи выполнимости. Помню так, что там надо либо найти хотя бы одну энку переменных, для которых формула истинна, либо показать, что она ложна для всех энок. Если формулировка правильна, то формула с отрицанием в точности соответствует задаче ТС: если $F,G$ принимают одинаковые значения тогда и только тогда, когда $\neg(F\leftrightarrow G)$ невыполнима. А если хотя бы для одной энки $F,G$ принимают разные значения, то $\neg(F\leftrightarrow G)$ выполнима. Если же отрицание убрать, то будет неправильно, соответствие потеряется. Лучше в исчислении предикатов формулировать: $F,G$ принимают одинаковые условия $\Leftrightarrow (\forall x) \neg (F(x) \leftrightarrow G(x))$. Тут уже отрицание не уберешь - это теперь видно явно.