CNF упрощение

Question

Учитывая набор предложений, я хочу сначала проверить, являются ли они выполнимыми. Если они есть, я хочу упростить их и создать CNF, например, (a ИЛИ b) ^ (НЕ b) следует упростить до: a ^ (НЕ b). Я работаю только с пропозициональными формулами. Я пытался использовать библиотеку Java SAT4j для этого. Он может показать мне, является ли набор предложений выполнимым, но, похоже, не имеет никакого способа вернуть мне упрощенный CNF. Что я могу сделать для эффективного упрощения CNF? Есть ли какие-либо реализации Java или Python для этого?

Answer 1

Вы можете использовать сопроцессор Riss3g Норберта Манти, чтобы упростить CNF,

SAT Solver Minisat 2 позволяет хранить предварительно обработанные CNF в файле.

Лингелинг, SAT у решателя из Австрии есть опция "-s" упростить CNF статьи.

Чтобы преобразовать логическое выражение в упрощенное CNF Вы можете использовать bc2cnf.