Оптимизатор z3.

[пианист]

Есть ли здесь кто-то, кто пользовался программой z3 (https://en.wikipedia.org/wiki/Z3_Theorem_Prover) в качестве оптимайзера?
Для инициирования содержательности, вопросик "на берегу": можно ли использовать указанный оптимизатор и стоит ли?
Задача, если что, б.-м. типичная, которую я пытаюсь решать (с переменным успехом), содержит примерно 2800 булевских переменных и 1500 условий.

(Оффтоп)

У меня есть, ест-но, более конкретные вопросы, но их есть смысл обсуждать с теми, кто данным модулем пользовался ирл.

[Sender]

Какого рода у вас задача, SMT или SAT? В последнем случае имеет смысл воспользоваться более специализированным решателем. На небольших задачах z3 вполне себе работает, по вашей ссылке на википедию есть ссылка на прекрасную книгу с примерами использования: SAT/SMT by Example.

[пианист]

Ни то, ни другое.
Я z3 использую (точнее, пытаюсь) в качестве MIP-решалки, такая функция в z3 тоже имеется.

[Sender]

Ну это же частный случай SMT, разве нет?

-- Ср ноя 16, 2022 13:56:35 --

Просто используются соответствующие теории. Впрочем, я тут мало что могу подсказать.

[пианист]

Честно говоря, не в курсе, но вполне допускаю.
Не слышал ни о ком из наших хлябей (логистика на транспорте), кто бы использовал выполнимость логических формул для чего-либо кроме ИБД (собс-но, и про использование для ИБД тоже не слышал, но тут все может быть).
Но в любом случае, большое спасибо, что откликнулись. Буду иметь в виду про SMT, может, где-то пригодится..

[traffic_lights]

Для MIP лучше использовать CPLEX. В сети есть ломаная версия. У меня стоит лицензионная CPLEX Studio IDE 20.1.0 (см., например, https://www.ibm.com/docs/en/SSSA5P_12.8 ... scplex.pdf).

[пианист]

traffic_lights
Согласен. Говорят, Gurobi еще лучше.
Просто я пока просматриваю решения по максимуму эконом класса; раздуть бюджет не штука.