Дополнение по поводу решаемости задачи SAT

[Aegypius Monachus]

Для любой булевой функции (БФ) Y(x1,…, xi,…,xm) существует «интегральная функция»,
с помощью которой можно за 2*m шагов получить одно из решений уравнения
Y(x1,…, xi,…,xm) = 1
(и за один шаг определить, имеет ли данная БФ хоть одно ненулевое значение – решение задачи SAT).
Данная БФ принадлежит к классу, для которого существует приемлемо компактная форма представления. Предполагается, что ее «интегральная функция» также имеет приемлемо компактную форму представления.
Для бесповторных БФ это уже доказано.
Для небесповторных БФ вопрос компактной формы следует искать в области упрощения символьных выражений (компьютерная алгебра), где утверждается, что не существует общего метода упрощения для всех классов символьных выражений.
Т.е. вопрос аналогичен по сути поиску компактной формулы интеграла некоторой функции.
Это интересно?

@темы: Вопросы

Comments

[dmd2001]

Это интересно!
К задаче SAT сводима задача факторизации. Есть способ свести задачу факторизации к задаче определения разрешимости-неразрешимости квадратного диофантового уравнения двух неизвестных, а также к задаче определения четности-нечетности одного из неизвестных подобного диофантового уравнения, при условии, что гарантированно известны наличие единственного решения этого уравнения и четность-нечетность второго из двух неизвестных. Как в общих словах будет выглядеть алгоритм составления булевой функции из конкретного диофантового уравнения под одну из этих задач?

[Aegypius Monachus]

Булеву функцию проще представить для диофантова уравнения x*y=z, где z -заданное, а x и y нужно найти. Полагаем натуральные числа x, y и z двоичными векторами.
mod2( di,zi,1) равен 1, если di и zi (соответствующие разряды d(прозведения x и y) и z) равны
и 0 в противном случае,
следовательно mod2( di,zi,1)*...*mod2( d1,z1,1) - искомая булева функция.
Такая функция компактна, а вот компактная формая для ее ФВИ пока не найдена.