Я хотел бы знать, как API-интерфейс Java SAT4j SAT решает свои псевдобулевы проблемы. Я просмотрел javadoc, но я совершенно не знаком с проблемами SAT.
Из документа о выпуске (https://www.researchgate.net/publication/220163278_The_Sat4j_library_release_22), Я думаю, что для всего используется специальный псевдобулев решатель, а не наоборот (псевдобулевы ограничения, переведенные в SAT CNF).
Есть у кого конкретные знания?