Малоизвестный факт
https://en.wikipedia.org/wiki/2-satisfiability
Если у вас все ограничения в КНФ имеют размер не более 2, то ваша проблема тривиально разрешима за полиномиальное время.
https://www.cs.utexas.edu/~marijn/publications/p01c05_lah.pdf - класс решателей, что выполняет поиск решения с предпросмотром, выбирает очередную переменную и её значение такими, чтобы количество бинарных ограничений после выбранного присваивания возросло как можно сильнее.
Посему, всё выглядит, что если вы можете создать или оптимизировать КНФ, чтобы она содержала как можно больше бинарных ограничений, то решать её может оказаться выгоднее.
Если у вас все ограничения в КНФ имеют размер не более 2, то ваша проблема тривиально разрешима за полиномиальное время.
https://www.cs.utexas.edu/~marijn/publications/p01c05_lah.pdf - класс решателей, что выполняет поиск решения с предпросмотром, выбирает очередную переменную и её значение такими, чтобы количество бинарных ограничений после выбранного присваивания возросло как можно сильнее.
Посему, всё выглядит, что если вы можете создать или оптимизировать КНФ, чтобы она содержала как можно больше бинарных ограничений, то решать её может оказаться выгоднее.