Решатель
Перейти к навигации
Перейти к поиску
Решатель (англ. Solver) — программное обеспечение, предназначенное для решения рассматриваемой математической задачи. На вход решателю поступает описание задачи в некоторой заданной форме, а на выходе он выдает решение задачи.
Виды решаемых задач[править]
- SAT-решатели — решают задачи выполнимости булевых формул. На выходе у них ответ — выполнима ли заданная формула и если выполнима, то выдается набор значений, на котором она выполнена (истинна).
- SMT-решатели — решают задачи разрешимости логических формул в расширяемом наборе теорий[1]. Включают теорию списков, массивов, линейной арифметики, неинтерпретируемых функций и т. п.
- Линейные и нелинейные уравнения и их системы
- Линейные и нелинейные оптимизационные проблемы
- Дифференциальные уравнения и их системы
- Нахождение минимального пути
- Нахождение минимального остовного дерева
- Также бывают решатели, предназначенные для решения головоломок, кроссвордов и задач по бриджу и преферансу.
См. также[править]
- Геометрический решатель САПР
- Логическое программирование
- Решение задач
- Логика в информатике
- Satisfiability Modulo Theories