Я читал в Википедии, что объединение - это процесс решения проблемы выполнимости.
В то же время я знаю, что такие решатели называются «решателями SAT» или «решателями SMT». Так это разные имена для одного и того же?
Если вы говорите, что они разные, пожалуйста, укажите на недостатки в моем лечении.
Ответы:
Решатели SAT решают проблему булевой удовлетворенности . Это «проблема определения, могут ли переменные данной булевой формулы быть назначены таким образом, чтобы формула оценивалась как ИСТИНА».
Например, найти присвоение значений истинности переменным таким образом, чтобы является истинным. Решатель SAT может вернуть решение, такое как , , .а , б , в ( a ∨ b ∨ c ) ∧ ( ¬ a ∨ ¬ b ∨ c ) ∧ ( a ∨ ¬ b ∨ ¬ c ) ∧ ( ¬ a ∨ b ∨ ¬ c ) = т т у й б = т т у й с = т т у й
Решатели SMT решают более общую проблему, а именно: теории удовлетворенности по модулю . Это «проблема решения логических формул относительно комбинаций фоновых теорий, выраженных в классической логике первого порядка с равенством». Эти теории могут включать «теорию действительных чисел, теорию целых чисел и теории различных структур данных, таких как списки, массивы, битовые векторы и так далее».
Пример, данные , введенные переменные и и , спрашивает , является ли следующее выполнима , Решатель SMT ответил бы да, с решением , , и .х : я п т Y: Я п т е: Я п т → я н т е( x + 2 ) ≠ f( у- 1 ) ∧ x = ( у- 4 ) х = - 2 Y= 2 е( 0 ) = 1 е( 1 ) = 3
Унификация - это особый метод, который принимает два термина и находит замену, которая делает условия равными. Например, при заданных терминах и объединение приведет к замене . Объединение, вероятно, используется внутри решателей SMT.б о о к ( Д. ~ Смит , у , 2010 ) { х ↦ Д. Смит , у ↦ «Рыбалка» }b o o k ( x , «Рыбалка» , 2010 ) b o o k ( Д. ~ Смит , у, 2010 ) { x ↦ Д. Смит , у↦ "Рыбалка" }
источник