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

website user guide Book

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

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

CPMpy

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