Алгоритм упрощения CNF

Question

Учитывая, что логическое выражение имеет конъюнктивную нормальную форму: существует ли "простой" алгоритм, чтобы упростить его, сохраняя при этом в CNF?

В частности, какое свойство следующего выражения вызывает это упрощение?

(~a+b+c)(a+~b+c)(a+~c)

упрощает до...

(~a+b+c)(a+~b)(a+~c)

Answer 1

Карта Карно вашего примера:

Чтобы получить упрощенный DNF, ячейки "1" сгруппированы так, чтобы получить покрытие с минимальным количеством минут.

Точно так же можно сгруппировать ячейки "0", чтобы получить обратное покрытие с минимальным количеством членов.

Обратная карта:

Литералы результирующих терминов должны быть инвертированы, чтобы достичь желаемого минимума CNF

(a + ~ b) (a + ~ c) (~ a + b + c)

В этой процедуре используется тот факт, что инверсия minterm является maxterm (обычно называемым предложением CNF) с инвертированными литералами.