Решатели SMT не более мощные, чем решатели SAT. Они по-прежнему будут выполняться в экспоненциальном порядке или будут неполными для тех же задач в SAT. Преимущество SMT заключается в том, что многие вещи, которые очевидны в SMT, могут занять много времени, прежде чем эквивалентный спутниковый решатель заново откроет для себя.
Таким образом, с проверкой программного обеспечения в качестве примера, если вы используете решатель SMT QF BV (бескванторная теория битовых векторов), решатель SMT будет знать, что (a + b = b + a) вместо этого на уровне слова, в то время как решателю SAT может потребоваться очень много времени, чтобы доказать это, используя отдельные логические значения.
Таким образом, что касается проверки программного обеспечения, вы можете легко создавать проблемы при проверке программного обеспечения, которые были бы сложны для любого SMT или SAT-решателя.
Во-первых, в QF BV необходимо развернуть циклы, а это означает, что практически вы должны ограничить то, что проверяет решатель. Если бы квантификаторы были разрешены, проблема стала бы PSPACE-полной, а не только NP-полной.
Во-вторых, проблемы, которые в целом считаются сложными, легко кодируются в QF BV. Например, вы можете написать программу следующим образом:
void run(int64_t a,int64_t b)
{
a * b == <some large semiprime>;
assert (false);
}
Теперь, конечно, решатель SMT легко докажет, что произойдет утверждение (ложь), но ему нужно будет предоставить контрпример, который даст вам входные данные a,b. Если вы установите <some large number> в полупростое число RSA, то вы просто перевернете умножение... иначе известное как целочисленная факторизация! Таким образом, это, вероятно, будет сложно для любого решателя SMT и демонстрирует, что проверка программного обеспечения в целом является сложной проблемой (если только P = NP или, по крайней мере, целочисленная факторизация не станет легкой). Такие решатели SMT — это просто шаг вперед по сравнению с решателями SAT, поскольку они облечены в более легкий для написания и понятный язык.
Решатели SMT, которые решают более сложные теории, обязательно неполны или даже медленнее, чем решатели SAT, потому что они пытаются решить более сложные проблемы.
Смотрите также:
- Интересно, что решатель Beaver SMT преобразует QF BV в CNF и может использовать решатель SAT в качестве задний конец.
- Klee, который может принять программу, скомпилированную в LLVM IR (промежуточное представление), и проверяет наличие ошибок, и находит примеры, противоречащие утверждениям, и т. д. Если он находит ошибку, он может привести контрпример к правильности (он даст вам входные данные, которые воспроизведут ошибку).
person
Realz Slaw
schedule
16.09.2012
