Булева функция, какова цель DNF и CNF?
Булевы функции могут быть выражены в дизъюнктивной нормальной форме (DNF) или конъюнктивной нормальной форме (CNF). Кто-нибудь может объяснить, почему эти формы полезны?
2 ответа
CNF полезен, потому что эта форма непосредственно описывает булеву задачу SAT, которая, хотя и NP-полная, имеет много неполных и эвристических экспоненциальных решателей времени. CNF был далее стандартизирован в формат файла, называемый " формат файла DIMACS CNF ", из которого может работать большинство решателей. Таким образом, например, индустрия микросхем может проверить свои схемы схем путем преобразования в DIMACS CNF и ввода в любой из доступных решателей. Преобразование Цейтина может преобразовать схемы в равноудаленный CNF.
DNF практически не так полезен, но преобразование формулы в DNF означает, что можно увидеть список возможных назначений, которые будут удовлетворять формуле. К сожалению, преобразование формулы в DNF в целом является трудным делом и может привести к экспоненциальному увеличению (очень большой DNF), что очевидно, поскольку экспоненциальное число удовлетворяющих назначений в формуле может быть экспоненциальным.
Хотя CNF может быть кратким по сравнению с DNF, иногда трудно рассуждать, потому что он может потерять структуру при преобразовании, например, из схемы, и поэтому будет полезна другая сжатая форма. Структура данных графа and-инвертора была разработана для этой цели; он может более точно моделировать структуру цепей, и поэтому его гораздо проще рассуждать в некоторых типах формул. Однако не так много решателей, которые работают с ним.
Другие формы включают в себя:
Это помогает выразить функции некоторым стандартным способом. При этом проще автоматически пройти через множество алгоритмов.
Обе формы могут быть использованы, например, при автоматическом решении теорем, а именно CNF в методе разрешения.