Оптимизация SAT / CNF

Задача

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

TRUE=(a OR b OR c OR d) AND (a OR f) AND ...

НОТов нет, и это конъюнктивная нормальная форма. Это легко разрешимо. Однако я пытаюсь минимизировать количество истинных присваиваний , чтобы сделать все утверждение истинным. Я не мог найти способ решить эту проблему.

Возможные решения

Я придумал следующие способы решения этой проблемы:

1. Преобразование в ориентированный граф и поиск минимального остовного дерева, охватывающего только подмножество вершин.Есть алгоритм Эдмонда, но он дает MST для всего графа, а не для подмножества вершин.
   • Может быть, есть версия алгоритма Эдмонда, которая решает проблему для подмножества вершин?
   • Может быть, есть способ построить граф из исходной проблемы, который можно было бы решить с помощью других алгоритмов?
2. Использовать SAT-решатель , решатель LIP или исчерпывающий поиск. Меня не интересуют эти решения, так как я пытаюсь использовать эту проблему в качестве лекционного материала.

Вопрос

Есть ли у вас идеи / комментарии? Можете ли вы придумать другие подходы, которые могут сработать?