K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями

Далее булева формула в КНФ <math>F(x_1, x_2, ..., x_n) \;</math> будет рассматриваться и как булева функция, и как множество дизъюнктов. Булева формула F является формулой в k-КНФ, если все дизъюнкты имеют величину не более k. Для дизъюнкта C обозначим за var(C) множество переменных, встречающихся в C. Если <math>v \in var(C) \;</math>, то ''ориентация'' <math>v \;</math> является положительной, если литерал v принадлежит к C, и отрицательной, если литерал <math>\bar{v} \;</math> принадлежит к C. Вспомним, что если F является булевой формулой в КНФ над переменными <math>(x_1, x_2, ..., x_n) \;</math>, а <math>a \;</math> – частичным присваиванием переменным, то ''ограничение'' F согласно <math>a \;</math> определяется как формула <math>F' = F \lceil_a \;</math> на множестве переменных, значения которых задаются без использования <math>a \;</math>, получаемая в результате обработки каждого дизъюнкта C формулы F следующим образом: если значение C в результате присваивания <math>a \;</math> становится равным 1, то C следует удалить; в противном случае заменить C дизъюнктом C’, полученным в результате удаления из C любых литералов, значения которых в результате присваивания <math>a \;</math> становятся равными 0. Единичным дизъюнктом называется дизъюнкт, содержащий ровно один литерал.