Розв'язувач

Розв'язувач (англ. solver) — програмне забезпечення, призначене для розв'язання розглядуваної математичної задачі. На вхід розв'язувачу надходить опис задачі в деякій заданій формі, а на виході він видає розв'язок задачі.

Види розв'язуваних задач:

• SAT Solvers — розв'язують задачі здійсненності бульових формул. На виході в них відповідь — чи виконана задана формула і якщо виконана, то видається набір значень, на якому вона правдива.
• SMT Solvers — розв'язують задачі з теорій, представлених у бібліотеці SMT-LIB (англ. Satisfiability Modulo Theories), що включає, наприклад, теорію списків, масивів, лінійної арифметики, неінтерпретованих функцій і т. д.
• лінійні і нелінійні рівняння і їхні системи
• Лінійні й нелінійні оптимізаційні проблеми
• диференціальні рівняння і їхні системи
• Знаходження мінімального шляху
• Знаходження мінімального покриваючого дерева
• Також бувають розв'язувачі, що призначені для розв'язання головоломок, кросвордів і задач із бриджу й преферансу.

General Problem Solver (GPS) — спеціальна комп'ютерна програма, створена в 1957 році Гербертом Саймоном (Herbert Simon), Дж. Шоу (J.C. Shaw), і Алленом Ньюелом (Allen Newell), призначена для роботи як універсальний розв'язувач задач, що теоретично може бути використана для розв'язування всіх можливих задач, які можуть бути формалізовані в символічній системі, що задана конфігурацією правил введення. Це була перша комп'ютерна програма, яка розділила свої знання задач (у формі правил проблемної області) від своєї стратегії, як розв'язувати завдання (як загальний пошуковий рушій).

Розв'язувачі зазвичай використовують архітектуру схожу на GPS, щоб відокремити формулювання задачі від стратегії, яка використовується для її розв'язування. Хоча стратегією, використаною в GPS, був загальний алгоритм з єдиною метою повноти, сучасні розв'язувачі, як правило, використовують спеціалізований підхід з урахуванням конкретного класу задач, для якого призначено розв'язувач. Перевага цього рішення полягає в тому, що розв'язувач не залежить від детальної інформації про кожний конкретний випадок задачі.

Для задач певного класу (наприклад, систем нелінійних рівнянь) є доступним, як правило, широкий спектр різних алгоритмів; іноді розв'язувач реалізує декілька алгоритмів, а іноді тільки один. Зазвичай, розв'язувачі просто використовують чисельні методи, хоча існують деякі розв'язувачі, які здатні виконувати деякі символічні перетворення для пошуку рішення.