Интернет магазин китайских планшетных компьютеров |
|
Компьютеры - Satisfiability Modulo Theories - Выразительная сила SMT11 мая 2011Оглавление: 1. Satisfiability Modulo Theories 2. Выразительная сила SMT SMT формула это обобщение булевой формулы SAT, в которой переменные заменены предикатами из соответствующих теорий. Поэтому SMT предоставляют больше возможностей для моделирования чем формулы SAT. Например, SMT формула позволяет моделировать операции функции модулей микропроцессора на уровне слов, а не на уровне битов. SMT решателиПервые попытки решения SMT задач были направлены на преобразование их в SAT формулы и решением формулы SAT решателем. Такой подход имеет свои преимущества — он позволяет использовать существующие SAT решатели без изменений и использовать сделанные в них оптимизации. С другой стороны потеря высокоуровневой семантики лежащих в основе теорий означает, что SAT решатель должен приложить немалые усилия, чтобы вывести "очевидные" факты. Это соображение привело к появлению специализированных SMT решателей, которые интегрируют обычные булевы доказательства в стиле алгоритма DPLL с решателями специализированными для теорий, работающие с дизъюнкциями и конъюнкциями предикатов из заданной теории. Архитектура дублированного DPLL) передает функции булева доказательства DPLL SAT решателю, который в свою очередь взаимодействует с решателем теории T через предопределенный интерфейс. Решатель теории T должен уметь проверять осуществимость конъюнкций из предикатов теории переданных из SAT решателя. Для того чтобы такая интеграция работала, решатель теории должен участвовать в анализе конфликтов, т.е. должен выводить новые факты из уже имеющихся, а также предоставлять объяснения невыполнимости при возникновении конфликтов. Другими словами, решатель теории должен быть инкрементальным и иметь возможность отката.
Просмотров: 1782
|