Пределы решателей SMT - программирование

Традиционно большая часть работы с вычислительной логикой была либо пропозициональной, и в этом случае вы использовали решатель SAT (логическая выполнимость) или первый порядок, в этом случае вы использовали доказательство теоремы первого порядка.

В последние годы был достигнут большой прогресс в решении SMT (выполнимости по модульной теории), которые в основном дополняют пропозициональную логику с теориями арифметики и т.д.; Джон Рашби из SRI International зашел так далеко, что назвал их разрушительной технологией.

Каковы наиболее важные практические примеры проблем, которые могут быть рассмотрены в логике первого порядка, но SMC не может обрабатываться? В частности, какие проблемы возникают, которые не могут быть обработаны SMT в области проверки программного обеспечения?

Ответ 1

Решатели SMT не являются более мощными, чем SAT-решатели. Они все равно будут работать в экспоненциальном времени или быть неполными для тех же проблем в SAT. Преимущество SMT заключается в том, что многие вещи, которые очевидны в SMT, могут занять много времени для повторного обнаружения эквивалентного сат-решателя.

Таким образом, с проверкой программного обеспечения в качестве примера, если вы используете SMF-решатель QF BV (без кванторов), решатель SMT будет знать, что (a + b = b + a) на уровне слова вместо этого, хотя для решения SAT может потребоваться очень долгое время, чтобы доказать, что использование отдельных логических значений.

Таким образом, при проверке программного обеспечения вы можете легко создавать проблемы при проверке программного обеспечения, что было бы трудно для любого решателя SMT или SAT.

Во-первых, петли должны быть развернуты в QF BV, что означает, что практически вы должны ограничить то, что проверяет решатель. Если квантификаторы были разрешены, он становится проблемой PSPACE-complete, а не только NP-полной.

Во-вторых, проблемы, которые считаются сложными вообще, легко кодировать в QF BV. Например, вы можете написать программу следующим образом:

void run(int64_t a,int64_t b)
{
  a * b == <some large semiprime>;

  assert (false);
}

Теперь, конечно, решатель SMT легко докажет, что assert (false) произойдет, но он должен будет предоставить встречный пример, который даст вам входы a,b. Если вы установите <some large number> в полупрограмму RSA, тогда вы просто измените размножение... иначе называемое целочисленной факторизацией! Таким образом, это вряд ли будет трудно для любого решателя SMT и продемонстрирует, что проверка программного обеспечения является сложной проблемой вообще (если только P = NP или, по крайней мере, целая факторизация не становится легкой). Такие решатели SMT - это всего лишь нога на SAT-решателях, одевая вещи на более легком в написании и понятном для пользователя языке.

Решатели SMT, которые решают более сложные теории, обязательно неполны или даже медленнее, чем SAT-решатели, потому что они пытаются решить более сложные проблемы.

См. также:

Интересно, что Bever SMT solver переводит QF BV на CNF и может использовать SAT-решение в качестве back-end.
Klee, который может взять программу, скомпилированную в LLVM IR (промежуточное представление), и проверяет наличие ошибок, и находит встречные примеры для утверждений и т.д. Если он обнаружит ошибку, он может дать встречный пример правильности (он даст вам ввод, который будет воспроизводить ошибку).