Как SAT4J решает псевдобулевы задачи? Использует ли он собственный псевдобулев решатель или переводит ограничения в CNF?

Я хотел бы знать, как API-интерфейс Java SAT4j SAT решает свои псевдобулевы проблемы. Я просмотрел javadoc, но я совершенно не знаком с проблемами SAT.

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

Есть у кого конкретные знания?


person Bread    schedule 21.04.2019    source источник


Ответы (1)


Sat4j не переводит количество элементов или псевдобулевы ограничения в CNF, он обрабатывает их изначально, используя либо систему доказательства разрешения, либо какую-то систему доказательства «секущих плоскостей», называемую обобщенным разрешением.

person Daniel Le Berre    schedule 23.04.2019