Hardprob/Maximum Renamable Horn Subformula

Набор булевых переменных U, коллекция C скобок-конъюнкций не больше чем из трех литералов.
Найти переименовываемую хорнову подформулу C' от C, т.е. подмножество C'⊆ C, т.к. здесь существует подмножество S ⊆ U, таких переменных, что перестановка литералов в делает C' хорновой булевой формулы, где .
Максимизировать размер подформулы, т.е. |C'|.