Программирование ответами: подход к сложным задачам поиска
Answer set programming
Программирование ответами (ASP): декларативный подход к сложным задачам поиска (NP-трудные). Решение через вычисление стабильных моделей, надежность и завершимость.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Парадигма программирования, ориентированная на сложные задачи поиска. Программирование на основе множеств ответов (ASP) — это форма декларативного программирования, ориентированная на сложные (преимущественно NP-трудные) задачи поиска. Она основана на семантике стабильных моделей (множеств ответов) логического программирования. В ASP задачи поиска сводятся к вычислению стабильных моделей, а для их решения используются решатели множеств ответов — программы для генерации стабильных моделей. Вычислительный процесс, применяемый при разработке многих решателей множеств ответов, является развитием алгоритма DPLL и, как правило, всегда завершается (в отличие от вычисления запросов в Prolog, которое может привести к бесконечному циклу). В более широком смысле, ASP охватывает все применения множеств ответов для представления знаний и логического вывода, а также использование оценки запросов в стиле Prolog для решения задач, возникающих в этих областях.
Programming paradigm focused on difficult search problems
Answer set programming (ASP) is a form of declarative programming oriented towards difficult (primarily NP hard) search problems. It is based on the stable model (answer set) semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers—programs for generating stable models—are used to perform search. The computational process employed in the design of many answer set solvers is an enhancement of the DPLL algorithm and, in principle, it always terminates (unlike Prolog query evaluation, which may lead to an infinite loop). In a more general sense, ASP includes all applications of answer sets to knowledge representation and reasoning and the use of Prolog style query evaluation for solving problems arising in these applications.
Большая группа
Клика в графе — это набор попарно смежных вершин. Следующая программа Lparse находит клику заданного размера в заданном ориентированном графе или определяет, что такая клика не существует: n {in(X) : v(X)}. : in(X), in(Y), X!=Y, not e(X,Y). Это ещё один пример организации типа "сгенерировать и проверить". Правило выбора в первой строке "генерирует" все множества, состоящие из вершин. Ограничение во второй строке "отсеивает" множества, которые не являются кликами.
A clique in a graph is a set of pairwise adjacent vertices. The following Lparse program finds a clique of size in a given directed graph, or determines that it does not exist:
n {in(X) : v(X)}. : in(X), in(Y), X!=Y, not e(X,Y). This is another example of the generate and test organization. The choice rule in Line 1 "generates" all sets consisting of vertices. The constraint in Line 2 "weeds out" the sets that are not cliques.
Гамильтоновский цикл
Гамильтонов цикл в ориентированном графе — это цикл, проходящий через каждую вершину графа ровно один раз. Следующая программа Lparse может быть использована для поиска гамильтонова цикла в заданном ориентированном графе, если он существует; мы предполагаем, что 0 является одной из вершин. {в(X,Y)} : e(X,Y). : 2 {в(X,Y) : e(X,Y)}, v(X). : 2 {в(X,Y) : e(X,Y)}, v(Y). r(X) : в(0,X), v(X). r(Y) : r(X), в(X,Y), e(X,Y). : не r(X), v(X). Правило выбора в строке 1 "генерирует" все подмножества множества ребер. Три ограничения "отсеивают" подмножества, которые не являются гамильтоновыми циклами. Последнее из них использует вспомогательный предикат ("достижим из 0") для исключения вершин, не удовлетворяющих этому условию. Этот предикат определяется рекурсивно в строках 6 и 7. Эта программа является примером более общей организации "сгенерировать, определить и проверить": она включает определение вспомогательного предиката, который помогает нам отбросить все "неподходящие" потенциальные решения.
A Hamiltonian cycle in a directed graph is a cycle that passes through each vertex of the graph exactly once. The following Lparse program can be used to find a Hamiltonian cycle in a given directed graph if it exists; we assume that 0 is one of the vertices. {in(X,Y)} : e(X,Y). : 2 {in(X,Y) : e(X,Y)}, v(X). : 2 {in(X,Y) : e(X,Y)}, v(Y). r(X) : in(0,X), v(X). r(Y) : r(X), in(X,Y), e(X,Y). : not r(X), v(X). The choice rule in Line 1 "generates" all subsets of the set of edges. The three constraints "weed out" the subsets that are not Hamiltonian cycles. The last of them uses the auxiliary predicate (" is reachable from 0") to prohibit the vertices that do not satisfy this condition. This predicate is defined recursively in Lines 6 and 7. This program is an example of the more general "generate, define and test" organization: it includes the definition of an auxiliary predicate that helps us eliminate all "bad" potential solutions.
Языковая стандартизация и конкурс ASP
Рабочая группа по стандартизации ASP разработала стандартную спецификацию языка под названием ASP Core 2, к которой стремятся современные системы ASP. ASP Core 2 является референсным языком для соревнований по программированию ответами (Answer Set Programming Competition), на которых решатели ASP периодически тестируются на наборе эталонных задач.
The ASP standardization working group produced a standard language specification, called ASP Core 2, towards which recent ASP systems are converging. ASP Core 2 is the reference language for the Answer Set Programming Competition, in which ASP solvers are periodically benchmarked over a number of reference problems.
Сравнение реализации
Ранние системы, такие как smodels, использовали метод перебора с возвратом для поиска решений. По мере развития теории и практики решателей булевой выполнимости (SAT), ряд решателей ASP были построены на основе решателей SAT, включая ASSAT и Cmodels. Они преобразовывали формулу ASP в пропозиции SAT, применяли решатель SAT, а затем преобразовывали решения обратно в форму ASP. Более современные системы, такие как Clasp, используют гибридный подход, применяя алгоритмы, управляемые конфликтами и вдохновленные SAT, без полного преобразования в булеву логическую форму. Эти подходы позволяют значительно повысить производительность, часто на порядок, по сравнению с более ранними алгоритмами перебора с возвратом. Проект Potassco выступает в качестве зонтичной организации для многих систем, включая clasp, системы заземления (gringo), инкрементальные системы (iclingo), решатели ограничений (clingcon), компиляторы языка действий в ASP (coala), распределенные реализации с использованием интерфейса передачи сообщений (claspar) и многие другие. Большинство систем поддерживают переменные, но только косвенно, посредством принудительного заземления, используя систему заземления, такую как Lparse или gringo, в качестве фронтенда. Необходимость заземления может привести к комбинаторному взрыву дизъюнктов; следовательно, системы, выполняющие заземление "на лету", могут иметь преимущество. Реализации программирования на основе множеств ответов, управляемые запросами, такие как система Galliwasp и s(CASP), полностью избегают заземления, используя комбинацию резолюции и коиндукции.
Early systems, such as smodels, used backtracking to find solutions. As the theory and practice of Boolean SAT solvers evolved, a number of ASP solvers were built on top of SAT solvers, including ASSAT and Cmodels. These converted ASP formula into SAT propositions, applied the SAT solver, and then converted the solutions back to ASP form. More recent systems, such as Clasp, use a hybrid approach, using conflict driven algorithms inspired by SAT, without fully converting into a Boolean logic form. These approaches allow for significant improvements of performance, often by an order of magnitude, over earlier backtracking algorithms. The Potassco project acts as an umbrella for many of the systems below, including clasp, grounding systems (gringo), incremental systems (iclingo), constraint solvers (clingcon), action language to ASP compilers (coala), distributed Message Passing Interface implementations (claspar), and many others. Most systems support variables, but only indirectly, by forcing grounding, by using a grounding system such as Lparse or gringo as a front end. The need for grounding can cause a combinatorial explosion of clauses; thus, systems that perform on the fly grounding might have an advantage. Query driven implementations of answer set programming, such as the Galliwasp system and s(CASP) avoid grounding altogether by using a combination of resolution and coinduction. Platform Features Mechanics Name OS Licence Variables Function symbols Explicit sets Explicit lists Disjunctive (choice rules) supportASPeRiX LinuxGPLon the fly groundingASSATSolarisFreewareSAT solver basedClasp Answer Set SolverLinux, macOS, WindowsMIT Licenseincremental, SAT solver inspired (nogood, conflict driven)CmodelsLinux, SolarisGPLincremental, SAT solver inspired (nogood, conflict driven)diff SATLinux, macOS, Windows (Java virtual machine)MIT LicenseSAT solver inspired (nogood, conflict driven). Supports solving probabilistic problems and answer set samplingDLVLinux, macOS, Windowsfree for academic and non commercial educational use, and for non profit organizationsnot Lparse compatibleDLV ComplexLinux, macOS, WindowsGPLbuilt on top of DLV — not Lparse compatibleGnTLinuxGPL built on top of smodelsnomore++LinuxGPLcombined literal+rule basedPlatypusLinux, Solaris, WindowsGPLdistributed, multi threaded nomore++, smodelsPbmodelsLinux?pseudo boolean solver basedSmodelsLinux, macOS, WindowsGPLSmodels cc Linux?SAT solver based; smodels w/conflict clausesSupLinux?SAT solver based
Механические особенности платформы
Early systems, such as smodels, used backtracking to find solutions. As the theory and practice of Boolean SAT solvers evolved, a number of ASP solvers were built on top of SAT solvers, including ASSAT and Cmodels. These converted ASP formula into SAT propositions, applied the SAT solver, and then converted the solutions back to ASP form. More recent systems, such as Clasp, use a hybrid approach, using conflict driven algorithms inspired by SAT, without fully converting into a Boolean logic form. These approaches allow for significant improvements of performance, often by an order of magnitude, over earlier backtracking algorithms. The Potassco project acts as an umbrella for many of the systems below, including clasp, grounding systems (gringo), incremental systems (iclingo), constraint solvers (clingcon), action language to ASP compilers (coala), distributed Message Passing Interface implementations (claspar), and many others. Most systems support variables, but only indirectly, by forcing grounding, by using a grounding system such as Lparse or gringo as a front end. The need for grounding can cause a combinatorial explosion of clauses; thus, systems that perform on the fly grounding might have an advantage. Query driven implementations of answer set programming, such as the Galliwasp system and s(CASP) avoid grounding altogether by using a combination of resolution and coinduction. Platform Features Mechanics Name OS Licence Variables Function symbols Explicit sets Explicit lists Disjunctive (choice rules) supportASPeRiX LinuxGPLon the fly groundingASSATSolarisFreewareSAT solver basedClasp Answer Set SolverLinux, macOS, WindowsMIT Licenseincremental, SAT solver inspired (nogood, conflict driven)CmodelsLinux, SolarisGPLincremental, SAT solver inspired (nogood, conflict driven)diff SATLinux, macOS, Windows (Java virtual machine)MIT LicenseSAT solver inspired (nogood, conflict driven). Supports solving probabilistic problems and answer set samplingDLVLinux, macOS, Windowsfree for academic and non commercial educational use, and for non profit organizationsnot Lparse compatibleDLV ComplexLinux, macOS, WindowsGPLbuilt on top of DLV — not Lparse compatibleGnTLinuxGPL built on top of smodelsnomore++LinuxGPLcombined literal+rule basedPlatypusLinux, Solaris, WindowsGPLdistributed, multi threaded nomore++, smodelsPbmodelsLinux?pseudo boolean solver basedSmodelsLinux, macOS, WindowsGPLSmodels cc Linux?SAT solver based; smodels w/conflict clausesSupLinux?SAT solver based
Имя ОС Лицензия Переменные Функциональные символы Явные множества Явные списки Поддержка дизъюнктивных (выборочных) правил
ASPeRiX Linux GPL Заземление "на лету"
ASSAT Solaris Freeware На основе решателя SAT
Clasp Answer Set Solver Linux, macOS, Windows MIT License Инкрементальный, вдохновленный решателем SAT (nogood, управляемый конфликтами)
Cmodels Linux, Solaris GPL Инкрементальный, вдохновленный решателем SAT (nogood, управляемый конфликтами)
diff Linux, macOS, Windows (виртуальная машина Java) MIT License Вдохновленный решателем SAT (nogood, управляемый конфликтами). Поддерживает решение вероятностных задач и выборку множеств ответов
DLV Linux, macOS, Windows Бесплатный для академического и некоммерческого образовательного использования, а также для некоммерческих организаций Не совместим с Lparse
DLV Complex Linux, macOS, Windows GPL Построен на основе DLV — не совместим с Lparse
GnT Linux GPL Построен на основе smodels
nomore++ Linux GPL Основан на комбинации литералов и правил
Platypus Linux, Solaris, Windows GPL Распределенный, многопоточный, основан на nomore++ и smodels
Pbmodels Linux? Псевдо-булев решатель
Smodels Linux, macOS, Windows GPL
Smodels cc Linux? На основе решателя SAT; smodels с дизъюнктами конфликтов
Sup Linux? На основе решателя SAT
Early systems, such as smodels, used backtracking to find solutions. As the theory and practice of Boolean SAT solvers evolved, a number of ASP solvers were built on top of SAT solvers, including ASSAT and Cmodels. These converted ASP formula into SAT propositions, applied the SAT solver, and then converted the solutions back to ASP form. More recent systems, such as Clasp, use a hybrid approach, using conflict driven algorithms inspired by SAT, without fully converting into a Boolean logic form. These approaches allow for significant improvements of performance, often by an order of magnitude, over earlier backtracking algorithms. The Potassco project acts as an umbrella for many of the systems below, including clasp, grounding systems (gringo), incremental systems (iclingo), constraint solvers (clingcon), action language to ASP compilers (coala), distributed Message Passing Interface implementations (claspar), and many others. Most systems support variables, but only indirectly, by forcing grounding, by using a grounding system such as Lparse or gringo as a front end. The need for grounding can cause a combinatorial explosion of clauses; thus, systems that perform on the fly grounding might have an advantage. Query driven implementations of answer set programming, such as the Galliwasp system and s(CASP) avoid grounding altogether by using a combination of resolution and coinduction. Platform Features Mechanics Name OS Licence Variables Function symbols Explicit sets Explicit lists Disjunctive (choice rules) supportASPeRiX LinuxGPLon the fly groundingASSATSolarisFreewareSAT solver basedClasp Answer Set SolverLinux, macOS, WindowsMIT Licenseincremental, SAT solver inspired (nogood, conflict driven)CmodelsLinux, SolarisGPLincremental, SAT solver inspired (nogood, conflict driven)diff SATLinux, macOS, Windows (Java virtual machine)MIT LicenseSAT solver inspired (nogood, conflict driven). Supports solving probabilistic problems and answer set samplingDLVLinux, macOS, Windowsfree for academic and non commercial educational use, and for non profit organizationsnot Lparse compatibleDLV ComplexLinux, macOS, WindowsGPLbuilt on top of DLV — not Lparse compatibleGnTLinuxGPL built on top of smodelsnomore++LinuxGPLcombined literal+rule basedPlatypusLinux, Solaris, WindowsGPLdistributed, multi threaded nomore++, smodelsPbmodelsLinux?pseudo boolean solver basedSmodelsLinux, macOS, WindowsGPLSmodels cc Linux?SAT solver based; smodels w/conflict clausesSupLinux?SAT solver based