Answer Set Programming with Clingo in Examples¶
- In logic programming knowledge is represented as explicit facts and rules.
- Computation is performed by applying logical reasoning to solve problems.
- ASP is a type of logic programming geared towards complex search problems.
Clingo is a system to perform ASP. It derives a set of answers consistent with the problem specification (the program).
The examples here should work with clingo 5.
Sources:
Windows 10/11¶
Miniconda¶
Probably the easiest option is using a miniconda Python environment, as explained in
https://www.youtube.com/watch?v=H7NmClCXONY
- install miniconda from https://docs.anaconda.com/miniconda/
- run Anaconda prompt from Start Menu
- conda install -c potassco clingo
- conda install jupyter
The last step is not necessary for clingo itself, but you probably want to run the course notebooks on your computer. A previously existing Jupyter installation from another Python distribution should work (?) with miniconda.
To start Jupyter Lab, run Anaconda Prompt from the Start Menu and enter
jupyter lab☆ Windows binary (optional)¶
You may already have a Python installation with Jupyter which you want to use. There is a stand-alone Windows binary:
- get latest zip from https://github.com/potassco/clingo/releases
- e.g. https://github.com/potassco/clingo/releases/download/v5.3.0/clingo-5.3.0-win64.zip
- unzip into folder of your choice
Add that folder to your PATH:
- in File Explorer navigate into folder
- in location bar, right-click and "Copy address"
- go to System settings (Win menu in left lower corner, cog wheel)
- search for "env", click "Edit environment variables for your account"
- click "Path"
- click "Edit"
- click "New"
- Ctrl-V to insert folder path
- Save, Done.
Now clingo should be an external program which is available in Jupyter with %%script and !
Easy Answer Set Programming¶
The system starts with the empty set and keeps creating answers by applying rules until there is no more change.
The order of the statements in a clingo program does not matter for the system, but for an easier understanding it helps to structure programs into the three sections:
- choice
- rules
- constraints
The three sections can also be understood as
- generate
- extend
- eliminate
See Potassco videos Easy Answer Set Programming
Choice¶
Let's create a file with some code. We do this here from within this notebook, but you can also use the text editor of your choice and run the file on the command line: clingo ex01.lp 0
In [1]:
%%file ex01.lp
{ rainy }.
Overwriting ex01.lp
■ Clingo creates answers by repeatedly applying rules until there is no more change.
rainy is a constant. Here it could be understood as a description of the current weather situation.
{ rainy } indicates choice: add the content to an answer, or not
- Applying the choice gives us an answer set with two answers: empty, rainy
- Applying the choice again to each answer does not change anything, so we are done
- The answers in the final answer set are also called the models
- Each model conforms to the specifications in the input file.
We run the example with the 0 option which means show all models. Otherwise, we get only the first.
In [2]:
!clingo ex01.lp 0
clingo version 5.4.1 Reading from ex01.lp Solving... Answer: 1 Answer: 2 rainy SATISFIABLE Models : 2 Calls : 1 Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.000s
Note the empty first answer. There are two models consistent with the program.
Jupyter Options¶
We do not want to create a large number of small example files in the current directory.
Script¶
We can always start a cell with the %%script cell magic.
- Sadly, clingo uses various non-zero return codes to indicate 'program consistent', instead of 0 which is standard for successful completion.
- The option --no-raise-error seems to be necessary to avoid confusing Jupyter messages.
This information, like so much of clingo documentation, is not easy to find.
See e.g. https://www.mat.unical.it/aspcomp2013/files/aspoutput.txt
In [3]:
%%script clingo 0 --no-raise-error
{ rainy }.
clingo version 5.4.1 Reading from stdin Solving... Answer: 1 Answer: 2 rainy SATISFIABLE Models : 2 Calls : 1 Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.000s
Script Alias¶
We define an alias so we can call clingo move conveniently:
In [4]:
%alias_magic --cell clingo script -p "clingo --no-raise-error 0"
Created `%%clingo` as an alias for `%%script clingo --no-raise-error 0`.
We still have to fall back on the %%script version occasionally.
Rules¶
Rules consist of head and body:
HEAD :- BODY
Here are some educated guesses from the current weather situation:
In [5]:
%%clingo
{ rainy }.
{ sunny }.
wet :- rainy.
dry :- sunny.
clingo version 5.4.1 Reading from stdin Solving... Answer: 1 Answer: 2 rainy wet Answer: 3 sunny dry Answer: 4 sunny dry rainy wet SATISFIABLE Models : 4 Calls : 1 Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.000s
- After the choices we have four answers: empty, rainy, sunny, rainy and sunny
- Applying the wet/dry rules to each answer gives the final answer set
- Applying the rules again would not change anything
- Again, each model conforms to the specifications in the input file
■ The order of rule application does not change the final result.
It is nevertheless sensible to write Clingo programs in a consistent style, such as starting with facts and choices, then rules, then constraint.
Constraints¶
Now we use our real-world knowledge: we cannot have both rainy and sunny.
We can specify this in clingo by using a constraint, which looks much like a rule, and can be read as Nothing IF, or better: not a solution IF
In [6]:
%%clingo
{ rainy }.
{ sunny }.
wet :- rainy.
dry :- sunny.
:- rainy, sunny.
clingo version 5.4.1 Reading from stdin Solving... Answer: 1 Answer: 2 rainy wet Answer: 3 sunny dry SATISFIABLE Models : 3 Calls : 1 Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.000s
The previous answer 4 is now missing because it contained both rainy and sunny.
Constants, Variables, Predicates¶
Clingo has somewhat weird conventions for constants and variables:
- first letter lower case: constant
- upper case: variable
Use quotes to describe constants starting with upper case letters, e.g. "X"
A predicate consists of a name and zero more arguments:
- The number of arguments is called the arity of the predicate
- e.g. t(austin,88) has arity 2
- we can have more than one predicate with the same name but different arity
- refer to a specific one by e.g. t/2
Predicates can be used to express facts by adding a dot:
- wet.
- t(austin,88).
In the following example we use the predicate t/2 to state some facts first, and then formulate rules to draw conclusions:
- A city is warm if the temperature is higher than in austin
- The rule is applied until there is no more change in the answer set
- In this example we do not have choices; there is just one answer
In [7]:
%%clingo
t(austin,88). t(dallas,95). t(houston,90). t(san_antonio,85).
warm(C) :- t(C,T1), t(austin,T2), T1>T2.
clingo version 5.4.1 Reading from stdin Solving... Answer: 1 t(austin,88) t(dallas,95) t(houston,90) t(san_antonio,85) warm(dallas) warm(houston) SATISFIABLE Models : 1 Calls : 1 Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.000s
Recursive Rules¶
When there are circles in the rule dependencies the situation can be described as recursive:
To derive the result the rules can be understood as being executed all at once.
Pooling, Directives, Intervals¶
As a programming language Clingo contains a number of non-essential features that make our life a little easier:
- Pooling: group of facts that contain the same predicate symbol
- Directive: show only atoms formed from given predicate symbol and number of arguments
- Interval: a range of values
In [8]:
%%clingo
t(austin,88; dallas,95; houston,90; san_antonio,85).
warm(C) :- t(C,T1), t(austin,T2), T1>T2.
#show warm/1.
clingo version 5.4.1 Reading from stdin Solving... Answer: 1 warm(dallas) warm(houston) SATISFIABLE Models : 1 Calls : 1 Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.000s
Intervals are frequently used for integers and be understood as a shorthand, e.g.
- instead of num(1). num(2). num(3). and so on
- we can use num(1..n)
In [949]:
%%clingo
num(1..5).
clingo version 5.4.1 Reading from stdin Solving... Answer: 1 num(1) num(2) num(3) num(4) num(5) SATISFIABLE Models : 1 Calls : 1 Time : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.001s
Grounding¶
Clingo is a combination of two parts:
- gringo, the grounder
- clasp, the solver
Before solving a model the variables are grounded i.e. replaced by constants. This process can be made visible by calling gringo:
In [970]:
%%script gringo --text
{ r(a) }.
r(b).
t(X) :- r(X).
r(b).
{r(a)}.
t(b).
t(a):-r(a).
- Normally we do not need to be aware of the interplay of grounder and solver.
- Sometimes it helps to see the ground instantiation of a program to better understand it.
- Note that such intermediate results can get too large to feasibly print.
In [960]:
%%script clingo --no-raise-error 0
{ r(a) }.
r(b).
t(X) :- r(X).
clingo version 5.4.1 Reading from stdin Solving... Answer: 1 r(b) t(b) Answer: 2 r(b) t(b) r(a) t(a) SATISFIABLE Models : 2 Calls : 1 Time : 0.003s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.001s
In [721]:
%%clingo -V0 0
% V0 = less verbose, 0 = show all models
parent(ann,bob). parent(bob,carol). parent(bob,dan).
child(X,Y) :- parent(Y,X).
parent(ann,bob) parent(bob,carol) parent(bob,dan) child(bob,ann) child(carol,bob) child(dan,bob) SATISFIABLE
Math¶
Clingo only knows about integers!
Here we use a different set of command line arguments to limit the size of the output.
In [945]:
%%script clingo --no-raise-error -V0 0
p(N,N*N+N+1) :- N=0..5.
p(0,1) p(1,3) p(2,7) p(3,13) p(4,21) p(5,31) SATISFIABLE
In [726]:
%%clingo
% M is also an integer
p(M,N) :- N=1..4, N=2*M.
p(1,2) p(2,4) SATISFIABLE
In [727]:
%%clingo
p(1..3).
p(1) p(2) p(3) SATISFIABLE
In [728]:
%%clingo
p(1;2;3).
p(1) p(2) p(3) SATISFIABLE
In [729]:
%%clingo
p(1). p(2). p(3).
p(1) p(2) p(3) SATISFIABLE
In [730]:
%%clingo
square(1..3,1..3).
square(1,1) square(1,2) square(1,3) square(2,1) square(2,2) square(2,3) square(3,1) square(3,2) square(3,3) SATISFIABLE
In [731]:
%%clingo
% answer sets are SETS i.e. no duplicates
p(1..2,1..4). p(1..4,1..2).
p(1,1) p(2,1) p(3,1) p(4,1) p(1,2) p(2,2) p(3,2) p(4,2) p(1,3) p(1,4) p(2,3) p(2,4) SATISFIABLE
Rules as Definitions¶
In [732]:
%%clingo
parent(ann,bob). parent(bob,carol). parent(bob,dan).
child(X,Y) :- parent(Y,X).
%parent(X,Y) :- father(X,Y).
%parent(X,Y) :- mother(X,Y).
ancestor(X,Y) :- parent(X,Y).
ancestor(X,Z) :- ancestor(X,Y), ancestor(Y,Z).
parent(ann,bob) parent(bob,carol) parent(bob,dan) child(bob,ann) child(carol,bob) child(dan,bob) ancestor(ann,bob) ancestor(bob,carol) ancestor(bob,dan) ancestor(ann,dan) ancestor(ann,carol) SATISFIABLE
In [733]:
%%clingo
% \ modulo, remainder after integer division
#const n = 10.
composite(N) :- N=1..n, I=2..N-1, N\I=0.
% N modulo I = 0 i.e. N is composite
composite(4) composite(6) composite(8) composite(9) composite(10) SATISFIABLE
Looks good.
Phase 2: Full Program¶
In [734]:
%%clingo
% \ modulo, remainder after integer division
#const n = 10.
composite(N) :- N=1..n, I=2..N-1, N\I=0.
prime(N) :- N=2..n, not composite(N).
composite(4) composite(6) composite(8) composite(9) composite(10) prime(2) prime(3) prime(5) prime(7) SATISFIABLE
Factorials¶
In [735]:
%%clingo
% anonymous variable _
#const n = 5.
fac(0, 1).
fac(N+1, F*(N+1)) :- fac(N, F), N < n .
fac(F) :- fac(_, F).
% #show fac/1.
fac(0,1) fac(1,1) fac(2,2) fac(3,6) fac(4,24) fac(5,120) fac(1) fac(2) fac(6) fac(24) fac(120) SATISFIABLE
Choice¶
In [736]:
%%clingo
% choice
{p(a);q(b)}.
q(b) p(a) p(a) q(b) SATISFIABLE
In [737]:
%%clingo
{p(1..3)}.
p(2) p(3) p(2) p(3) p(1) p(1) p(3) p(1) p(2) p(1) p(2) p(3) SATISFIABLE
In [738]:
%%clingo
{p(a;b;c)}.
p(b) p(c) p(b) p(c) p(a) p(a) p(c) p(a) p(b) p(a) p(b) p(c) SATISFIABLE
In [739]:
%%clingo
% lower and upper bound
1 {p(1..3)} 2.
p(2) p(3) p(2) p(3) p(1) p(1) p(3) p(1) p(2) SATISFIABLE
In [740]:
%%clingo
3 {p(1..4)} 3.
p(2) p(3) p(4) p(1) p(2) p(3) p(1) p(3) p(4) p(1) p(2) p(4) SATISFIABLE
In [741]:
%%clingo
1 {p(X);q(X)} 1 :- X=1..2.
p(1) q(2) p(1) p(2) q(1) q(2) q(1) p(2) SATISFIABLE
In [742]:
%%clingo
1 {p(X,1..2)} 1 :- X=1..2.
p(1,2) p(2,1) p(1,2) p(2,2) p(1,1) p(2,1) p(1,1) p(2,2) SATISFIABLE
Constraints¶
In [743]:
%%clingo
% as above
1 {p(1..3)} 2.
p(2) p(3) p(2) p(3) p(1) p(1) p(3) p(1) p(2) SATISFIABLE
In [744]:
%%clingo
1 {p(1..3)} 2.
:- p(1).
p(3) p(2) p(2) p(3) SATISFIABLE
In [745]:
%%clingo
1 {p(1..3)} 2.
:- not p(1).
p(1) p(1) p(3) p(1) p(2) SATISFIABLE
In [746]:
%%clingo
1 {p(1..3)} 2.
:- p(1), not p(2).
p(3) p(2) p(2) p(3) p(2) p(1) SATISFIABLE
Search as Choice and Constraints¶
In [747]:
%%clingo
% Partition (1,..,n) into r sum-free sets, e.g. (3), (2), (1, 4)
#const n = 4.
#const r = 3.
1 { in(I, 1..r)} 1 :- I = 1.. n .
:- in(I, X), in(J, X), in(I+J, X).
in(2,2) in(1,3) in(3,1) in(4,3) in(2,2) in(1,3) in(3,2) in(4,3) in(1,1) in(2,2) in(3,3) in(4,3) in(1,1) in(2,2) in(3,2) in(4,3) in(1,1) in(2,2) in(3,1) in(4,3) in(1,1) in(2,2) in(3,2) in(4,1) in(1,1) in(2,2) in(3,3) in(4,1) in(2,2) in(1,3) in(3,3) in(4,1) in(2,2) in(1,3) in(3,2) in(4,1) in(2,2) in(1,3) in(3,1) in(4,1) in(1,2) in(2,3) in(3,1) in(4,2) in(1,2) in(2,3) in(3,3) in(4,2) in(1,2) in(2,3) in(3,2) in(4,1) in(1,2) in(2,3) in(3,3) in(4,1) in(1,2) in(2,3) in(3,1) in(4,1) in(1,1) in(2,3) in(3,3) in(4,1) in(1,1) in(2,3) in(3,2) in(4,1) in(1,1) in(2,3) in(3,2) in(4,2) in(1,1) in(2,3) in(3,3) in(4,2) in(1,1) in(2,3) in(3,1) in(4,2) in(2,1) in(1,3) in(3,2) in(4,3) in(2,1) in(1,3) in(3,1) in(4,3) in(2,1) in(1,2) in(3,1) in(4,3) in(2,1) in(1,2) in(3,2) in(4,3) in(2,1) in(1,2) in(3,3) in(4,3) in(2,1) in(1,2) in(3,3) in(4,2) in(2,1) in(1,2) in(3,1) in(4,2) in(2,1) in(1,3) in(3,1) in(4,2) in(2,1) in(1,3) in(3,2) in(4,2) in(2,1) in(1,3) in(3,3) in(4,2) SATISFIABLE
In [748]:
%%clingo
#const n = 5.
#const r = 2.
1 { in(I, 1..r)} 1 :- I = 1.. n .
:- in(I, X), in(J, X), in(I+J, X).
UNSATISFIABLE
Speed up search: run several threads¶
In [749]:
%%file schur.lp
1 { in(I, 1..r)} 1 :- I = 1.. n .
:- in(I, X), in(J, X), in(I+J, X).
Overwriting schur.lp
In [750]:
!clingo -c r=4 -c n=44 schur.lp -t2
clingo version 5.4.1 Reading from schur.lp Solving... Answer: 1 in(1,1) in(2,4) in(3,3) in(4,3) in(5,1) in(6,4) in(7,4) in(8,1) in(9,2) in(10,4) in(11,2) in(12,2) in(13,3) in(14,3) in(15,1) in(16,2) in(17,1) in(18,4) in(19,2) in(20,3) in(21,1) in(22,4) in(23,4) in(24,1) in(25,3) in(26,4) in(27,4) in(28,1) in(29,2) in(30,3) in(31,1) in(32,3) in(33,2) in(34,2) in(35,4) in(36,2) in(37,2) in(38,4) in(39,4) in(40,1) in(41,3) in(42,3) in(43,4) in(44,1) SATISFIABLE Models : 1+ Calls : 1 Time : 0.059s (Solving: 0.01s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.051s Threads : 2 (Winner: 1)
Scheduling¶
In [751]:
%%clingo
person(jane). person(john).
day(mon). day(tue). day(wed). day(thu). day(fri). day(sat). day(sun).
available(jane) :- not on(fri).
available(john) :- not on(mon), not on(wed).
meet :- available(X) : person(X).
on(X) : day(X), not weekend(X) :- meet .
weekend(sat). weekend(sun).
#show meet.
#show on/1.
meet on(thu) meet on(tue) SATISFIABLE
Seating Arrangements¶
In [752]:
%%file seating.lp
#const n=6.
1 { at(1.. n, C)} 1 :- C =1.. n . % guest n at chair C
C1 = C2 :- at(G, C1), at(G, C2). % same as :- at(G,C1), at(G,C2), C1!=C2.
adj(X, Y) :- X=1.. n, Y=1..n, |X-Y|=1. % |x| absolute value
adj(1, n ; n, 1). % round table
like(1, 2; 3, 4).
dislike(2, 3; 1, 3).
:- like(G1, G2), at(G1, C1), at(G2, C2), not adj(C1, C2).
:- dislike(G1, G2), at(G1, C1), at(G2, C2), adj(C1, C2).
Overwriting seating.lp
In [753]:
!clingo seating.lp
clingo version 5.4.1 Reading from seating.lp Solving... Answer: 1 adj(1,6) adj(6,1) adj(2,1) adj(1,2) adj(3,2) adj(2,3) adj(4,3) adj(3,4) adj(5,4) adj(4,5) adj(6,5) adj(5,6) like(1,2) like(3,4) dislike(2,3) dislike(1,3) at(2,3) at(3,6) at(1,2) at(4,1) at(5,4) at(6,5) SATISFIABLE Models : 1+ Calls : 1 Time : 0.003s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.003s
Independent Sets of Vertices¶
(b,d,e,g) and (a,c,f,h) are independent i.e. not connected by edges
In [754]:
%%clingo
% a------b
% |\ /|
% | e--f |
% | | | |
% | | | |
% | h--g |
% |/ \|
% d------c
#const n = 4.
vertex(a;b;c;d;e;f;g;h).
edge(a, b; b, c; c, d; d, a;
e, f; f, g; g, h; h, e;
a, e; b, f; c, g; d, h).
n { in(X) : vertex(X) } n .
:- in(X), in(Y), edge(X, Y).
#show in/1.
in(b) in(d) in(e) in(g) in(a) in(c) in(f) in(h) SATISFIABLE
Graph Colouring¶
Graph as above, colors (red, blue), no adjacent vertices with same color
In [755]:
%%clingo
vertex(a;b;c;d;e;f;g;h).
edge(a, b; b, c; c, d; d, a;
e, f; f, g; g, h; h, e;
a, e; b, f; c, g; d, h).
color(red). color(blue).
1 { color(X, C) : color(C) } 1 :- vertex(X).
:- edge(X, Y), color(X, C), color(Y, C).
#show color/2.
color(a,red) color(b,blue) color(c,red) color(d,blue) color(f,red) color(e,blue) color(g,blue) color(h,red) color(b,red) color(a,blue) color(c,blue) color(d,red) color(e,red) color(f,blue) color(g,red) color(h,blue) SATISFIABLE
N-Queens¶
Place n queens on n * n chess board so that no queens attack each other
In [756]:
%%clingo
% 4 . Q . .
% 3 . . . Q
% 2 Q . . .
% 1 . . Q .
% 1 2 3 4
#const n = 4.
1 { queen(R, 1..n) } 1 :- R = 1..n . % one queen in each row
:- queen(R1,C), queen(R2,C), R1!=R2. % different row, same column
:- queen(R1,C1), queen(R2,C2), R1!=R2, |R1-R2|=|C1-C2|. % different row, same diagonal
#show queen/2.
queen(1,2) queen(2,4) queen(3,1) queen(4,3) queen(2,1) queen(3,4) queen(1,3) queen(4,2) SATISFIABLE
Performance¶
- Solving time depends on the encoding
- Inefficient encoding can severly limit the maximum feasible problem size
Here is a particularly bad encoding:
In [757]:
%%script clingo -V1 --no-raise-error --quiet=1 0
#const n=8.
row(1..n).
col(1..n).
n { queen(I,J) : row(I), col(J) } n.
:- queen(I,J1), queen(I,J2), J1 != J2.
:- queen(I1,J), queen(I2,J), I1 != I2.
:- queen(I,J), queen(II,JJ), (I,J) != (II,JJ), I+J == II+JJ. % diagonal down
:- queen(I,J), queen(II,JJ), (I,J) != (II,JJ), I-J == II-JJ. % diagonal up
#show queen/2.
clingo version 5.4.1 Reading from stdin Solving... Answer: 92 queen(7,7) queen(2,1) queen(4,2) queen(6,3) queen(8,4) queen(3,5) queen(5,8) queen(1,6) SATISFIABLE Models : 92 Calls : 1 Time : 0.467s (Solving: 0.46s 1st Model: 0.00s Unsat: 0.06s) CPU Time : 0.409s
The following encodings are much more efficient:
In [758]:
%%script clingo -V1 --no-raise-error --quiet=1 0
#const n = 8.
1 { queen(R, 1..n) } 1 :- R = 1..n . % one queen in each row
:- queen(R1,C), queen(R2,C), R1!=R2. % different row, same column
:- queen(R1,C1), queen(R2,C2), R1!=R2, |R1-R2|=|C1-C2|. % different row, same diagonal
clingo version 5.4.1 Reading from stdin Solving... Answer: 92 queen(4,4) queen(6,7) queen(3,2) queen(5,1) queen(1,6) queen(2,8) queen(7,5) queen(8,3) SATISFIABLE Models : 92 Calls : 1 Time : 0.009s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.007s
In [759]:
%%script clingo -V1 --no-raise-error --quiet=1 0
#const n = 8.
number(1..n).
1{q(K,J): number(K)}1:- number(J). % rows
:-q(I,J), q(I,J1), J<J1. % columns
:-q(I,J), q(I1,J1), J<J1, |I1-I|==J1-J. % diagonals
clingo version 5.4.1 Reading from stdin Solving... Answer: 92 number(1) number(2) number(3) number(4) number(5) number(6) number(7) number(8) q(5,1) q(7,2) q(2,3) q(4,4) q(8,5) q(1,6) q(3,7) q(6,8) SATISFIABLE Models : 92 Calls : 1 Time : 0.017s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.007s
The following encoding is even more efficient:
In [760]:
%%script clingo -V1 --no-raise-error --quiet=1 0
#const n = 8.
1 { queen(I,1..n) } 1 :- I = 1..n.
1 { queen(1..n,J) } 1 :- J = 1..n.
:- 2 { queen(D-J,J) }, D = 2..2*n.
:- 2 { queen(D+J,J) }, D = 1-n..n-1.
clingo version 5.4.1 Reading from stdin Solving... Answer: 92 queen(4,8) queen(2,5) queen(1,3) queen(6,7) queen(3,2) queen(8,6) queen(7,4) queen(5,1) SATISFIABLE Models : 92 Calls : 1 Time : 0.011s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.006s
Efficient encoding means we can go to much higher problem size:
In [761]:
%%script clingo -V1 --no-raise-error
#const n = 100.
1 { queen(I,1..n) } 1 :- I = 1..n.
1 { queen(1..n,J) } 1 :- J = 1..n.
:- 2 { queen(D-J,J) }, D = 2..2*n.
:- 2 { queen(D+J,J) }, D = 1-n..n-1.
clingo version 5.4.1 Reading from stdin Solving... Answer: 1 queen(1,93) queen(7,91) queen(35,99) queen(12,75) queen(38,95) queen(27,83) queen(45,100) queen(5,58) queen(2,52) queen(14,62) queen(3,50) queen(18,64) queen(41,86) queen(34,78) queen(13,56) queen(39,80) queen(50,89) queen(15,53) queen(10,46) queen(30,65) queen(44,76) queen(59,90) queen(47,77) queen(19,48) queen(23,51) queen(52,79) queen(29,55) queen(11,36) queen(58,82) queen(75,98) queen(66,88) queen(9,30) queen(49,69) queen(48,67) queen(42,60) queen(21,38) queen(16,32) queen(55,70) queen(28,42) queen(4,17) queen(80,92) queen(73,84) queen(61,71) queen(85,94) queen(77,85) queen(17,24) queen(37,43) queen(82,87) queen(31,34) queen(94,96) queen(53,54) queen(97,97) queen(8,7) queen(6,4) queen(24,21) queen(70,66) queen(33,28) queen(74,68) queen(22,15) queen(89,81) queen(40,31) queen(20,10) queen(46,35) queen(32,20) queen(57,44) queen(71,57) queen(62,47) queen(90,74) queen(25,8) queen(67,49) queen(92,73) queen(79,59) queen(26,5) queen(56,33) queen(69,45) queen(54,29) queen(99,72) queen(68,40) queen(43,14) queen(36,6) queen(72,41) queen(95,61) queen(60,25) queen(63,27) queen(100,63) queen(51,13) queen(65,26) queen(64,22) queen(93,37) queen(81,23) queen(98,39) queen(78,18) queen(84,19) queen(83,16) queen(76,3) queen(86,11) queen(88,12) queen(87,1) queen(96,9) queen(91,2) SATISFIABLE Models : 1+ Calls : 1 Time : 0.758s (Solving: 0.07s 1st Model: 0.07s Unsat: 0.00s) CPU Time : 0.686s
Ground Instantiation¶
- Performance depends on the size of the ground instantiation = what the solver has to look at
- We can get an idea of the size by printing the number of models before constraints
In [762]:
%%script clingo --no-raise-error --quiet=1 0
#const n=4.
row(1..n).
col(1..n).
n { queen(I,J) : row(I), col(J) } n.
%:- queen(I,J1), queen(I,J2), J1 != J2.
%:- queen(I1,J), queen(I2,J), I1 != I2.
%:- queen(I,J), queen(II,JJ), (I,J) != (II,JJ), I+J == II+JJ. % diagonal down
%:- queen(I,J), queen(II,JJ), (I,J) != (II,JJ), I-J == II-JJ. % diagonal up
clingo version 5.4.1 Reading from stdin Solving... Answer: 1820 row(1) row(2) row(3) row(4) col(1) col(2) col(3) col(4) queen(4,1) queen(1,2) queen(3,2) queen(1,3) SATISFIABLE Models : 1820 Calls : 1 Time : 0.007s (Solving: 0.01s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.007s
In [763]:
%%script clingo --no-raise-error --quiet=1 0
#const n = 4.
number(1..n).
1{q(K,J): number(K)}1:- number(J). % rows
%:-q(I,J), q(I,J1), J<J1. % columns
%:-q(I,J), q(I1,J1), J<J1, |I1-I|==J1-J. % diagonals
clingo version 5.4.1 Reading from stdin Solving... Answer: 256 number(1) number(2) number(3) number(4) q(1,1) q(3,2) q(3,3) q(4,4) SATISFIABLE Models : 256 Calls : 1 Time : 0.003s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.001s
In [764]:
%%script clingo --no-raise-error --quiet=1 0
#const n = 4.
1 { queen(R, 1..n) } 1 :- R = 1..n . % one queen in each row
%:- queen(R1,C), queen(R2,C), R1!=R2. % different row, same column
%:- queen(R1,C1), queen(R2,C2), R1!=R2, |R1-R2|=|C1-C2|. % different row, same diagonal
clingo version 5.4.1 Reading from stdin Solving... Answer: 256 queen(1,1) queen(2,3) queen(3,3) queen(4,4) SATISFIABLE Models : 256 Calls : 1 Time : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.001s
In [765]:
%%script clingo --no-raise-error --quiet=1 0
#const n = 4.
1 { queen(I,1..n) } 1 :- I = 1..n.
1 { queen(1..n,J) } 1 :- J = 1..n.
%:- 2 { queen(D-J,J) }, D = 2..2*n.
%:- 2 { queen(D+J,J) }, D = 1-n..n-1.
clingo version 5.4.1 Reading from stdin Solving... Answer: 24 queen(1,1) queen(3,2) queen(2,3) queen(4,4) SATISFIABLE Models : 24 Calls : 1 Time : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.001s
Aggregates¶
Function applied to sets, such count and sum.
In [766]:
%%clingo
% A -----B
% |\ /|
% | E--F |
% | | /| |
% | |/ | |
% | H--G |
% |/ \|
% D------C
vertex(a; b; c; d; e; f; g; h).
edge(a, b; b, c; c, d; d, a;
e, f; f, g; g, h; h, e;
a, e; b, f; c, g; d, h; f, h).
adjacent(X, Y) :- edge(X, Y).
adjacent(X, Y) :- edge(Y, X).
number_of_edges(N/2) :- N = #count {X, Y: adjacent(X, Y )}.
degree(X, D) :- vertex(X), D = #count {Y: adjacent(X, Y)}.
#show degree /2. #show number_of_edges /1.
number_of_edges(13) degree(a,3) degree(b,3) degree(c,3) degree(d,3) degree(e,3) degree(f,4) degree(g,3) degree(h,4) SATISFIABLE
In [767]:
%%clingo
p(a,1). p(b,1). p(c,2).
q(N) :- N = #count{A,X : p(A,X)}.
r(N) :- N = #count{A : p(A,X)}.
s(N) :- N = #count{X : p(A,X)}.
p(a,1) p(b,1) p(c,2) q(3) r(3) s(2) SATISFIABLE
Optimization¶
In [768]:
%%clingo
% a------b
% |\ /|
% | e--f |
% | | /| |
% | |/ | |
% | h--g |
% |/ \|
% d------c
#const n = 4.
vertex(a;b;c;d;e;f;g;h).
edge(a, b; b, c; c, d; d, a;
e, f; f, g; g, h; h, e;
a, e; b, f; c, g; d, h; h, f).
% Find largest independent sets of vertices
{ in(X) } :- vertex(X).
% set of n vertices of G
:- in(X), in(Y), edge(X, Y).
% no pairs of adjacent vertices
#maximize { 1, X : in(X) }.
% number of elements of in/1 is maximal
#show in/1.
Optimization: 0 in(d) Optimization: -1 in(b) in(d) Optimization: -2 in(b) in(d) in(e) Optimization: -3 in(b) in(d) in(e) in(g) Optimization: -4 OPTIMUM FOUND
Subset with maximal sum <= m¶
In [769]:
%%clingo
#const m = 22.
n(1). n(3). n(5). n(10). n(20).
{ in(X) } :- n(X). % subset of n/1.
:- #sum { X : in(X) } > m .
#maximize { X : in (X) }.
#show in/1.
Optimization: 0 in(1) Optimization: -1 in(5) Optimization: -5 in(1) in(5) Optimization: -6 in(3) in(5) Optimization: -8 in(1) in(3) in(5) Optimization: -9 in(10) Optimization: -10 in(1) in(10) Optimization: -11 in(5) in(10) Optimization: -15 in(1) in(5) in(10) Optimization: -16 in(3) in(5) in(10) Optimization: -18 in(1) in(3) in(5) in(10) Optimization: -19 in(20) Optimization: -20 in(1) in(20) Optimization: -21 OPTIMUM FOUND
Graph Colouring with minimum number of colours¶
In [770]:
%%clingo
% a------b
% |\ /|
% | e--f |
% | | /| |
% | |/ | |
% | h--g |
% |/ \|
% d------c
vertex(a;b;c;d;e;f;g;h).
edge(a, b; b, c; c, d; d, a;
e, f; f, g; g, h; h, e;
a, e; b, f; c, g; d, h; h, f).
size(N) :- N = #count { X : vertex(X) }.
1 { color(X, C) : C = 1..N } 1 :- vertex(X), size(N).
% every vertex has one color
:- edge(X, Y), color(X, C), color(Y, C).
% no adjacent vertices share the same color
#minimize { 1, C : color(X,C)}.
#show color/2.
color(b,6) color(a,8) color(c,8) color(d,7) color(e,7) color(f,8) color(g,7) color(h,6) Optimization: 3 OPTIMUM FOUND
Assign papers to referees¶
In [771]:
%%clingo
#const k = 2. % number of referees per submission
ref(1; 2; 3). % referees
sub(1; 2; 3; 4; 5; 6). % submissions
bid(1, 1, y; 1, 2, m; 1, 3, m; 2, 1, m; 2, 2, n; 2, 3, y; 3, 1, y; 3, 2, y; 3, 3, n).
bid(1, 4, m; 1, 5, y; 1, 6, m; 2, 4, y; 2, 5, y; 2, 6, n; 3, 4, y; 3, 5, m; 3, 6, m).
% ref X will review paper Y with willingness Z = yes/maybe/no
k { review(R, S) : ref(R), not bid(R, S, n) } k :- sub(S).
% every submission is assigned to k referees who bid yes/maybe
workload(R, N) :- ref(R), N = #count { S : review(R, S) }.
:- workload(R1, N1), workload(R2, N2), |N1 - N2| > 1.
% distribute somewhat evenly
#maximize { 1, R, S : bid(R, S, y), review (R, S) }.
% number of yes cases is maximal
#show review/2.
review(1,2) review(1,3) review(1,5) review(1,6) review(2,1) review(2,3) review(2,4) review(2,5) review(3,1) review(3,2) review(3,4) review(3,6) Optimization: -7 OPTIMUM FOUND
KnapSack¶
Find items so that weight limit is not exceeded and total value is maximised
In [772]:
%%clingo
item(1..5).
v(1,4; 2,2; 3,1; 4,10; 5,2).
w(1,12; 2,2; 3,1; 4,4; 5,1).
{ in(I) } :- item(I).
weight(W) :- W = #sum { X,I : in(I), w(I,X) }.
:- weight(W), W > 15.
value(V) :- V = #sum { X,I : in(I), v(I, X) }.
#maximize { V : value(V) }.
#show in/1. #show weight/1. #show value/1.
value(0) weight(0) Optimization: 0 in(3) value(1) weight(1) Optimization: -1 in(5) value(2) weight(1) Optimization: -2 in(3) in(5) value(3) weight(2) Optimization: -3 in(2) in(3) in(5) value(5) weight(4) Optimization: -5 in(1) in(3) in(5) value(7) weight(14) Optimization: -7 in(1) in(2) in(5) value(8) weight(15) Optimization: -8 in(2) in(3) in(4) in(5) value(15) weight(8) Optimization: -15 OPTIMUM FOUND
Find Shortest/Cheapest Path aka TSP, Traveling Salesman¶
- Find cheapest route/cycle to visit all nodes
- some connections are one direction only
Create clingo data file with Python, draw graph:
In [816]:
import networkx as nx
import matplotlib.pyplot as plt
cost = ((1,2,2), (1,3,3), (1,4,1),
(2,4,2), (2,5,2), (2,6,4),
(3,1,3), (3,4,2), (3,5,2),
(4,1,1), (4,2,2),
(5,3,2), (5,4,2), (5,6,1),
(6,2,4), (6,3,3), (6,5,1))
f = open('graphdata.lp', 'w')
f.write('node(1..6).\n')
for c in cost:
f.write('edge(%d,%d).\n' % (c[0], c[1]))
f.write('cost(%d,%d,%d).\n' % (c[0], c[1], c[2]))
f.close()
G = nx.DiGraph()
for c in cost:
G.add_edges_from([c[:2]], weight=c[2])
labels=dict([ ((u,v,),d['weight']) for u,v,d in G.edges(data=True)])
options = {
"font_size": 16,
"node_size": 1000,
"node_color": "white",
"edgecolors": "black",
"linewidths": 1,
"width": 1,
}
nx.draw_networkx(G, pos, **options)
nx.draw_networkx_edge_labels(G,pos,edge_labels=labels)
plt.show()
Assuming we have node(), edge(), and cost():
In [817]:
%%file tsp.lp
1 { cycle(X,Y) : edge(X,Y) } 1 :- node(X).
1 { cycle(X,Y) : edge(X,Y) } 1 :- node(Y).
reached(Y) :- cycle(1,Y).
reached(Y) :- cycle(X,Y), reached(X).
:- node(Y), not reached(Y).
cost(S) :- S = #sum { C : cycle(X,Y), cost(X,Y,C) }.
#minimize { C : cost(C) }.
#show cycle/2.
#show cost/1.
Overwriting tsp.lp
In [818]:
!clingo graphdata.lp tsp.lp 0
clingo version 5.4.1 Reading from graphdata.lp ... Solving... Answer: 1 cycle(1,2) cycle(2,5) cycle(3,4) cycle(6,3) cycle(4,1) cycle(5,6) cost(6) Optimization: 6 OPTIMUM FOUND Models : 1 Optimum : yes Optimization : 6 Calls : 1 Time : 0.004s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.003s
In [ ]: