У меня есть проблема оптимизации, которая подвергается линейным ограничениям. Как узнать, какой метод лучше для моделирования и решения проблемы. Обычно я спрашиваю о решении проблемы как проблемы выполнимости (SAT или SMT) по сравнению с решением проблемы линейного программирования (ILP ИЛИ MILP).
У меня нет больших знаний в обоих. Поэтому, пожалуйста, упростите свой ответ, если он у вас есть.
Вообще говоря, разница в том, что SAT ищет только возможные решения, в то время как ILP пытается оптимизировать что-то с учетом ограничений. Я полагаю, что некоторые решатели ILP фактически используют решатели SAT для получения начального допустимого решения. Проблема сенсорного массива, которую вы описываете в комментарии, сформулирована как ILP: «минимизируйте этот объект до этого». Вместо этого SAT-версия выбрала бы максимально допустимое количество датчиков и использовала бы его в качестве ограничения. Теперь это проблема выполнимости, но не та, которую легко выразить в конъюнктивной нормальной форме. Я бы рекомендовал использовать решатель с теорией целых чисел. Мой любимый Z3.
Однако, прежде чем отказываться от оптимизации, стоит попробовать GMPL/GLPK. Вы можете быть удивлены тем, насколько решаема ваша проблема. Если вам не так повезло, превратите это в проблему выполнимости и выведите Z3.
sum(x) <= 1очень проблематичен в SAT, и исследования предложили много разных кодировок. - person sascha schedule 01.12.2018