Add exact cover problem example

This commit is contained in:
Patrick Lühne 2020-05-07 02:54:13 +02:00
parent b55bc82b1d
commit a9ca72891c
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 15 additions and 0 deletions

5
examples/exact-cover.lp Normal file
View File

@ -0,0 +1,5 @@
{in(1..n)}.
:- I != J, in(I), in(J), s(X, I), s(X, J).
covered(X) :- in(I), s(X, I).
:- s(X, Y), not covered(X).

10
examples/exact-cover.spec Normal file
View File

@ -0,0 +1,10 @@
axiom: forall X (is_int(X) <-> exists N X = N).
input: n -> integer, s/2, is_int/1.
assume: n >= 0.
assume: forall X, Y (s(X, Y) -> is_int(Y)).
assert: forall X (in(X) -> X >= 1 and X <= n).
assert: forall X (exists I s(X, I) -> exists I (in(I) and s(X, I))).
assert: forall I, J (exists X (s(X, I) and s(X, J)) and in(I) and in(J) -> I = J).