В данном примере добавлен ещё один терм h с ограничением значений от 2 до 10, указано, что сумма должна быть больше h, после чего h максимизирован и выведен в &show. Директива &minimize может минимизировать несколько значений, перечисленных через точку с запятой:
Минимизация суммы нескольких термов:
#include <csp>.
&sum {a; b; c} = 113. vars(a;b;c).
&show {X : vars(X)}.
&dom {1..100} = X :- vars(X). &minimize{1*c;100*a}.
#show.
Результирующие наборы ответов:
Answer: 1 a=2 b=11 c=100
Optimization: 300
Answer: 2 a=2 b=100 c=11
Optimization: 211
Answer: 3 a=1 b=100 c=12
Optimization: 112
OPTIMUM FOUND
С использованием директивы &distinct можно обеспечить уникальность заданных значений.
#include <csp>. v(a,5). v(b,5).
&dom {2..M} = x(I) :- v(I,M). &sum {x(a);x(b)} > 7. &distinct {x(a);x(b)}.
&show {x(a);x(b)}.
#show.
Результирующие наборы ответов:
Answer: 1 x(a)=5 x(b)=4
Answer: 2 x(a)=5 x(b)=3
Answer: 3 x(a)=4 x(b)=5
Answer: 4 x(a)=3 x(b)=5
Здесь директива #show отключает лишний вывод и факты v/2 не отображаются (сравните с предыдущими примерами). Если убрать требование
26
уникальности значений x(a) и x(b), то добавятся результаты x(a)=5 x(b)=5 и x(a)=4 x(b)=4.
3.2. Задача SEND+MORE=MONEY
Задача SEND+MORE=MONEY предполагает, что каждая буква даннного выражения – это цифра от 0 до 9, при этом разные буквы – это разные цифры. Необходимо подобрать такой набор значений букв, чтобы цифровое равенство было верным.
Решение без использования ограничений может выглядеть следующим образом:
letter(s; e; n; d; m; o; r; y). values(0..9). % Обеспечить одно появление каждой буквы
1 { x(L,Val) : values(Val) } 1 :- letter(L). % 0..1 не более 1 появления каждого значения
{ x(L,Val) : letter(L) } 1 :- values(Val). % Все значения разные
:- letter(L), letter(L1), x(L,V1), x(L1,V1), L!= L1. smm :- values(S;E;N;D;M;O;R;Y), x(s,S), x(e,E),
x(n,N), x(d,D), x(m,M), x(o,O), x(r,R), x(y,Y), M > 0, S > 0, S*1000+E*100+N*10+D + M*1000+O*100+R*10+E == M*10000+O*1000+N*100+E*10+Y.
:- not smm.
#show x/2.
Вычисление требует много времени (несколько минут).
Answer: 1 x(o,0) x(m,1) x(y,2) x(e,5) x(n,6) x(d,7)
x(r,8) x(s,9)
Задача может быть решена с использованием ограничений:
#include <csp>. letter(s;e;n;d;m;o;r;y).
&dom {0..9} = X :- letter(X).
&sum {1000*s; 100*e; 10*n; 1*d; 1000*m; 100*o; 10*r; 1*e; -10000*m; -1000*o; -100*n; -10*e; -1*y} = 0.
&sum {m} != 0.
&distinct {X : letter(X)}. &show {X : letter(X)}. #show.
27
И результат:
Answer: 1 s=9 e=5 n=6 d=7 m=1 o=0 r=8 y=2
На формирование ответа потребовалось 0,016 сек.
3.3.Упражнения
1.Дано два пятизначных числа X и Y, состоящих из цифр от 0 до 9. Необходимо вычислить минимальную разницу X-Y, все цифры должны быть использованы и только по одному разу.
2.Дано выражение DONALD+GERALD=ROBERT. Предполагается, что каждая буква выражения – это цифра, при этом разные буквы – это разные цифры. Необходимо подобрать такой набор значений букв, чтобы цифровое равенство было верным.
3.Гамильтонов цикл в ориентированном графе это цикл, который проходит через каждую вершину графа ровно один раз. Найти гамильтонов цикл
взаданном ориентированном графе, если он существует.
4.Механизмы вывода и доказательства, используемые в ASP
4.1.Общее описание
В ASP решение задачи сводится к поиску устойчивой модели посредством набора программ ее генерации (решателей) [4,5]. Процесс поиска реализуется надстройкой над DPLL-алгоритмом, который всегда конечен, является полным алгоритмом поиска с возвратом для решения задачи определения выполнимости булевых формул (задача SAT – сокращение от слова SATISFIABLE – выполнимость), записанных в конъюнктивной нормальной форме (КНФ), и основан на правиле резолюций.
После приведения исходной булевой формулы к КНФ происходит генерация SAT-решателей, определяющих возможность назначения всем переменным, встречающимся в формуле, значения ложь или истина так, чтобы формула стала истинной.
4.2. Принципы построения SAT-решателей
SAT-решатели строятся с использованием алгоритма CDCL (ConflictDriven Clause Learning – управляемое конфликтами обучение дизъюнктам), который основан на алгоритме DPLL и отличается, с одной стороны, использованием структуры данных – импликационного графа, фиксирующего
28
назначения переменным, и нехронологического возврата с запоминанием дизъюнктов в ходе анализа конфликта [6].
Решается задача поиска устойчивой модели, т. е. назначения всем переменным, встречающимся в формуле в форме КНФ, значения «ложь» (0) или «истина» (1) так, чтобы формула стала истинной. Данный поиск основан на DPLL-алгоритме и является поиском с возвратом на КНФ, на каждом шаге которого происходит присваивание значения «ложь» или «истина» выбранной переменной с последующим ветвлением, после чего упрощённая формула проходит рекурсивную проверку на выполнимость. Если встречается конфликт, т. е. полученная формула является невыполнимой, включается механизм возврата (бэктрекинга), при котором отменяются ветвления, в которых для переменной были опробованы оба значения. В DPLL-алгоритме используются хронологические возвраты, когда формула объявляется невыполнимой после возврата к ветвлению первого уровня.
В CDCL-алгоритме все встречающиеся в процессе поиска дизъюнкты могут быть: а) выполнимые (satisfied), когда среди входящих в дизъюнкт значений есть «истина»; б) невыполнимые (unsatisfied) – все значения «ложь»; в) единичные (unit) – все значения «истина», кроме одной переменной, которой значение ещё не присвоено, г) неразрешённые (unresolved) – все остальные.
После ветвления для вычисления логических следствий сделанного выбора выполняется процедура распространения переменной (unit propagation), которая основана на правиле единичного дизъюнкта, при котором выбор переменной и её значения однозначен.
4.3.Схема CDCL-алгоритма
Вобщем виде CDCL-алгоритм можно представить следующим образом:
Алгоритм CDCL(φ, ν) вход: φ - формула (КНФ)
ν- значения переменных в виде множества пар выход: SAT (формула выполнима) или UNSAT (невыполнима)
если UnitPropagationConflict(φ,ν)
то возврат UNSAT
L := |
0 |
--уровень решения |
пока |
NotAllVariablesAssigned(φ,ν) |
|
(x,v) := |
PickBranchingVariable(φ,ν)--принятие решения |
|
L := L + |
1 |
|
|
|
29 |
ν := |
ν {(x,v)} |
|
если |
UnitPropagationConflict(φ,ν)--вывод последствий |
|
то β |
:= ConflictAnalysis(φ,ν) --диагностика конфликта |
|
если β < 0 то возврат UNSAT |
||
иначе Backtrack(φ,ν,β) |
--возврат (бэктрекинг) |
|
|
L := β |
|
возврат SAT
Здесь значение переменных ν(vi) {0,u,1} для всех vi, где u обозначает ещё не назначенную переменную. Уровень решения L, на котором переменной было присвоено значение от −1 (не присвоено) до количества переменных.
Современные информационные технологии развиваются очень быстро, появляется множество новых способов решения задач, однако их поиск должен строиться на владении традиционными технологиями. Как писал философ Бернард Шартрский: «Мы как карлики, сидящие на плечах гигантов, и потому можем видеть больше и дальше, чем они».
Данное издание призвано способствовать формированию у читателя знаний, умений и навыков по программированию наборов ответов с использованием ASP.
Список литературы
1.Potassco website. URL: https://potassco.org.
2.Gebser M., Harrison A., Kaminski R., Lifschitz V., Schaub T. Abstract Gringo. Theory and Practice of Logic Programming, 15(4-5):449–463, 2015. Available at http://arxiv.org/abs/1507.06576. 9, 119.
3.My Answer Set Programming Page.
URL: http://www.hakank.org/answer_set_programming/
4.Зачем нам всем нужен SAT и все эти P-NP. URL: https://habr.com/ru/post/207112/.
5.SAT Solvers: Theory and Practice. URL: https://resources.mpiinf.mpg.de/departments/rg1/conferences/vtsa08/slides/barret1_sat.pdf.
6.CDCL basics. URL: https://ru.coursera.org/lecture/automated-reasoning- sat/cdcl-basics-2ag2H .
30