Constraint Programming
What is it for?
Puzzle solving
- n-queens
- sudoku
Compiler problems
Routing Problems Allocation problems
Plannning Reachability Verification
Minizinc
webassembly playground tutorial 202 autumn school
Exploring a shipping puzzle, part 3
var int : x;
solve satisfy;
How to make DSLs. Look for macros. Look for function call. Look for gensyms
Minizinc has records now. That’s huge. Hmm. But it doesn’t have unions… What about recurisive records? Probably not
type Foo = tuple(int,int);
var Foo: biz;
var Foo: null = (0,0);
enum tag = Foo |
record(tag: "Foo", foo:null)
type Cell = tuple(int, int);
type Heap = array[Cell];
mov("a","b");
var vs par is compile vs runtime distinction in type system it would be cool if minizinc could support adts or records.
Embedding datalog into minizinc
set of int : verts = 1..3;
array[verts,verts] of bool : edge;
%array[int,int] of verts : edge0;
array[verts,verts] of var bool : path;
%edge0 = [|1,2 | 2,3];
% check if in edges list
function bool: edge0(int : i, int : j) =
i = 1 /\ j = 2 \/
i = 2 /\ j = 3;
edge = array2d(verts,verts, [ edge0(i,j) | i,j in verts]);
constraint forall(i,k in verts)(
path[i,k] <- % <-> ?
edge[i,k] \/ exists(j in verts)(edge[i,j] /\ path[j,k])
);
%output ["\(edge)"];
solve satisfy;
Note that -a
or --all-solutions
will show all solutions.
Non negated datalog should have a unique solution. Datalog with negation is a different ballgame.
Picat
index mode annotations table annotions include lattice type stuff “mode-directed tabling”
action rules loops
main =>
printf("hello world\n"),
X = 3,
print(X),
print([I**2 : I in 1..5 ]), % comprehensions
Y = {1,2,3,4}, % arrays
Y := 10, % assignement
print(Y),
print($foo(bar,$biz)), % Dollar sign $ for structs/
M = new_map(), put(M,mykey,10), print(get(M,mykey)),
print(fib(10))
.
% clauses.
index (+,-) (-,+)
edge(a,b).
edge(a,c).
edge(b,c).
edge(c,b).
% functions
fib(0) = F => F=1. % alternative fib(0) = 1. "function facts"
fib(1) = F => F=1.
fib(N) = F, N>1 => F = fib(N-1)+fib(N-2).
sum_list(L) = Sum => % returns sum(L)
S=0,
foreach (X in L)
S:=S+X
end,
Sum=S.
% tabling
table
fib2(0) = 1.
fib2(1) = 1.
fib2(N) = fib2(N-1)+fib2(N-2).
picat is by default pattern match based rather than unification based.
foo(1) => true.
% this fails
main => foo(X), print(X).
Answer Set Programming
See notes on answer set programming
Topics
Branch and Bound
Local Search
Lattices
Propagators
Heuristics
Misc
- google or-tools
- eclipse https://www.eclipseclp.org/
Hakan’s site an insane number fo examples in systems
Coursera Course
ORTools is apprently killer according to Minizinc Challenge
GeCode
constraint programming for robotics Also see interval constraint programming interval mooc http://www.codac.io/tutorial/index.html
csplib a library of constrains
art of propagators geocode manual on propagators (appendix P) Propagators have been described as “just” monotonic functions between lattices. https://www.youtube.com/watch?v=s2dknG7KryQ&ab_channel=ConfEngine
constraint acquisition inferring predoncitions for code?
Using and Understanding ortools’ CP-SAT: A Primer and Cheat Sheet