From a9ca72891ce06053caab7d6eb88cd5ab0db2b0c1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Thu, 7 May 2020 02:54:13 +0200
Subject: [PATCH] Add exact cover problem example

---
 examples/exact-cover.lp   |  5 +++++
 examples/exact-cover.spec | 10 ++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 examples/exact-cover.lp
 create mode 100644 examples/exact-cover.spec

diff --git a/examples/exact-cover.lp b/examples/exact-cover.lp
new file mode 100644
index 0000000..396f69b
--- /dev/null
+++ b/examples/exact-cover.lp
@@ -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).
diff --git a/examples/exact-cover.spec b/examples/exact-cover.spec
new file mode 100644
index 0000000..570719f
--- /dev/null
+++ b/examples/exact-cover.spec
@@ -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).