Решатель

Решатель (англ. Solver) — программное обеспечение, предназначенное для решения рассматриваемой математической задачи. На вход решателю поступает описание задачи в некоторой заданной форме, а на выходе он выдает решение задачи.

Виды решаемых задач

• SAT-решатели — решают задачи выполнимости булевых формул. На выходе у них ответ — выполнима ли заданная формула и если выполнима, то выдается набор значений, на котором она выполнена (истинна).
• SMT-решатели — решают задачи разрешимости логических формул в расширяемом наборе теорий. Включают теорию списков, массивов, линейной арифметики, неинтерпретируемых функций и т. п.
• Линейные и нелинейные уравнения и их системы
• Линейные и нелинейные оптимизационные проблемы
• Дифференциальные уравнения и их системы
• Нахождение минимального пути
• Нахождение минимального остовного дерева
• Также бывают решатели, предназначенные для решения головоломок, кроссвордов и задач по бриджу и преферансу.

См. также

• Геометрический решатель САПР
• Логическое программирование
• Решение задач
• Логика в информатике
• Satisfiability Modulo Theories

Ссылки

• Автоматический решатель математических задач на сайте Кафедры Математической теории интеллектуальных систем механико-математического факультета МГУ им. М. В. Ломоносова