Как присвоить целочисленные значения переменным логической формулы, используя sat4j в java?

Я совершенно новичок в решателе sat4j и исследую логические выполнимые задачи; и я застрял. Я хочу сделать программу, которая решает целые переменные, которые находятся в логической формуле, например;

x1 ‹ x2 + x3 пользователь вводит эту формулу, и моя программа удовлетворяет этой формуле (возвращает true), например x1 = 5 , x2 = 3, x3 = 4. Таким образом, формула возвращает true, и пользователь получает это целочисленное значение, которое удовлетворяет формуле. это можно сделать в sat4j, потому что я работаю в eclipse с java.


java sat sat-solvers satisfiability sat4j
person Aysim Toker    schedule 17.11.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Не уверен, что SAT4J решает SMT... Вам следует искать решатели SMT, которые поддерживают линейную арифметику (в вашем случае, похоже, подойдет только логика различий). Вы можете проверить: Z3 (решатель SMT от Microsoft), CVC4 и Yices. Более обширный список находится здесь: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

Надеюсь это поможет...

person fturkmen    schedule 18.11.2015
comment
У sat4j есть модуль, который обрабатывает проблемы удовлетворения ограничений, который покрывает это, но он делает это, уменьшая CSP до экземпляра SAT. Использование SMT-решателя — лучший подход для любых задач, кроме игрушечных, потому что преобразование CSP в SAT отбрасывает слишком много структурной информации, которую интеллектуальный решатель может использовать для поиска. - person Kyle Jones; 18.11.2015