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

Question

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

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

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

У кого-нибудь есть конкретные знания?

1

java sat4j

Источник

user7846618 21 апр '19 в 15:41

1 ответ

Другие вопросы по тегам java sat4j

user3867609 23 апр '19 в 05:30 2019-04-23 05:30 · Answer 1 · 2019-04-23 05:30

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