Entry tags:

bdd, haskell, логика, таблицы истинности

Вот, решил перетащить статейку.
С ubicon.biz. Поскольку мне неизвестно, что с ним будет, а статью жалко.

Про таблицы истинности и логику и Хаскель

Всякое логическое выражение можно характеризовать таблицей истинности:

00001111 x1
00110011 x2
01010101 x3
--------
11110000 ~x1
00000011 x1&x2
11110101 ~x1|x3

Таблицу истинности какого-либо выражения можно вычислить просто применив выражение к каждому столбцу.

А сами таблицы истинности можно замечтельно кодировать. Сейчас расскажу, как.

Таблицу истинности, длина которой всегда 2^n, можно поделить пополам - на две подтаблицы. Те, в свою очередь, снова пополам и так до тех пор, пока не упремся - в смысле, не дойдем до таблицы истинности длиной в 1, которую поделить нельзя. Такая минимальная таблица может иметь значение либо 0, либо 1.

Вот. Сейчас продемонстрирую на примере таблицы ~x1|x3:

1   1 1   1 0   1 0   1
  \ /   \ /   \ /   \ /
   *     *     *     *
    \   /       \   /
     \ /         \ /
      *           *
       \___   ___/
           \ /
            *

Самое первое упрощение, которое можно сделать - это не хранить узлы *, подузлы которых одновременно равны либо 0, либо 1. Мы всегда можем раздуть такие узлы при выполнении логических операций. Второе упрощение - это убрать одну из ветвей из *, если обе ветви равны. Мы в этом случае поставим знак =.

Тогда наше дерево станет таким:

             0   1
               \ /
                *
                |
                |
            1   =
             \ /
              *

Значительно меньшим по размерам.

Теперь перейдем к реализации таких деревьев на Хаскеле.

Они будут описаны с помощью алгебраических типов:

>data LT =
>   Z -- Z for zero
> | O -- O for one
> | D LT LT -- D for subdivision of logical table
> | E LT -- E for table where left part (present) is equal to right
> deriving (Eq, Ord, Show) -- default code for equality and ordering is sufficient.

Z будет представлять собой (под)таблицу, все элементы которой нули. D Z F - таблица для x1. D F Z - таблица для ~x1. Нумерация здесь условна, и номер 1 при переменной x означает только, что она первая на этом уровне. Сейчас продемонстрирую:

>-- Логические константы:
>lfalse = Z
>ltrue = O
>
>-- Создание таблиц истинности для переменных:
>lvar n
>   | n == 1 = D Z O
>   | n>0 = E (lvar (n-1))
>   | otherwise = error "Invalid variable number"

Таблицы истинности для x1, x2 и x3 будут, соответственно, D Z O, E (D Z O) и E (E (D Z O)). Попробуйте их распахнуть до длин 8 и убедиться, что они правильны. ;)

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

>-- Сперва рассмотрим вариант с разделением таблиц:
>lsimp (D a b) = case (lsimp a,lsimp b) of
>  (x,y)
>     | x == y ->
>         -- у нас могут быть варианты с равными
>         -- подтаблицами, которые можно дальше упростить,
>         -- например, если подтаблицы константы 0 или 1.
>         lsimp (E x)
>     | otherwise -> D x y
>-- Вариант с равными подтаблицами:
>lsimp (E a) = case lsimp a of
>  Z -> Z
>  O -> O
>  x -> E x
>-- Вот. Остались неупрощаемые варианты. Их мы охватим одной строкой:
>lsimp x = x

Теперь стоит определить логические операции. Сперва мы определим построение структуры таблицы результата в соотвествии с правилами применения операций, а затем применим упрощения:

>-- Логическая инверсия. Эта операция не требует упрощения результата.
>lnot Z = O
>lnot O = Z
>-- А все остальное - обработаем рекурсивно:
>lnot (D a b) = D (lnot a) (lnot b)
>lnot (E a) = E (lnot a)
>
>-- Вычисление логического И. Сперва - вычисление структуры:
>land' Z _ = Z -- \"ноль\" логического И
>land' _ Z = Z
>land' O x = x -- \"единица\" логического И
>land' x O = x
>land' (D a b) (D x y) = D (land' a x) (land' b y)
>-- Напомню, что мы можем преобразовать (E a) в (D a a):
>land' (D a b) (E x) = D (land' a x) (land' b x)
>land' (E a) (D x y) = D (land' a x) (land' a y)
>land' (E a) (E x) = E (land' a x)
>
>-- Логическое И. С упрощением:
>land a b = lsimp (land' a b)
>
>-- А логическое ИЛИ мы определим через логическое И и логическое НЕ (воспользовавшись x|y = ~((~x)&(~y)):
>lor a b = lnot (land (lnot a) (lnot b))

Еще раз “вот.”

Теперь стоит ответить на вопрос, “а зачем это все?”

Иногда надо выяснить, выполняется ли какая-либо логическая формула (то есть, принимает ли хоть когда-либо значение 1, “истина”), и если выполняется, то при каких значениях переменных.

На первую часть вопроса ответить легко - если в результате вычисления формулы с помощью lvar, lnot, land и lor мы не получили Z, то формула выполняется.

На вторую часть вопроса ответить сложнее. Но не сильно.

Любое логическое выражение мы можем привести к одной из канонических форм - конъюнктивной нормальной форме (КНФ) или дизъюнктивной нормальной форме (ДНФ). Первая представляет собой логическое И набора объединенных логическим ИЛИ из переменных и(или) их логических отрицаний. Вторая, наоборот, соединяет по ИЛИ набор логических И переменных и их отрицаний. Любая, входящая в ДНФ конъюнкция (логическое И от переменных и их отрицаний) представляет из себя набор выполняющих формулу значений перменных. А на вход, обычно, подаются задачи в КНФ.

Если мы смотрим на какую-то формулу и знаем, что она выполнима, то это значит, что где-то в ее дереве таблицы истинности находится вариант O. На пути до этого варианта мы можем натолкнуться на варианты D a b и E a. Первый вариант, вариант D означает, что хотя бы одна из подтаблиц содержит вариант выполнения формулы, и что текущая переменная играет роль - в набор выполнимости подтаблицы a она входит со знаком логического отрицания, а в набор выполнимости подтаблицы b - напрямую. Вариант E означает, что где-то там, дальше, находится вариант O, но влияния на путь до него текущая переменная не оказывает.

Вот это мы сейчас и запишем.

>-- Вычисление наборов выполнимости для формулы.
>lsatsets t = lsatsets' 1 t
>
>lsatsets' var Z = []
>lsatsets' var O = [[]]
>lsatsets' var (D a b) =
>    (map ((-var):) (lsatsets' (var+1) a)) ++
>    (map (var:) (lsatsets' (var+1) b))
>lsatsets' var (E a) = lsatsets' (var+1) a

С чего мы, там, начали? С x1&x2 и ~x1|x3?

Вот вам результаты вычисления их наборов истинности:

Main> lsatsets (lvar 1 `land` lvar 2)
[[1,2]]
(129 reductions, 297 cells)
Main> lsatsets (lnot (lvar 1) `lor` lvar 3)
[[-1],[1,3]]
(184 reductions, 317 cells)
Main>

Теперь мы можем решать небольшие задачи на выполнимость логических формул.

Вышеперечисленное сильно напоминает библиотеку BuDDy - библиотеку работы с Binary Decision Diagram. Только меньше размерами кода в несколько раз и, я думаю, значительно меньшим быстродействием - для начала работы самое оно.

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

ERROR \"a.lhs\":18 - Syntax error in input (unexpected backslash (lambda))
Prelude> :r
ERROR \"a.lhs\":58 - Syntax error in expression (unexpected `;', possibly due to b
ad layout)
Prelude> :r
Main> lsatsets (lvar 1 `land` lvar 2)
[[1,2]]
(129 reductions, 297 cells)
Main> lsatsets (lnot (lvar 1) `lor` lvar 3)
[[-1],[1,3]]
(184 reductions, 317 cells)
Main>

Две опечатки, ни одной ошибки типов или ошибки при выполнении.

Всегда бы так. ;)