From c8da38880b6ca0d8223fce06cc9ad0b14e8a1b78 Mon Sep 17 00:00:00 2001
From: jika <vandechat@tutanota.com>
Date: Thu, 9 Mar 2023 15:38:54 +0100
Subject: [PATCH] sat pip3

---
 pip3/1.db   |  1 +
 pip3/q1.db  |  2 ++
 pip3/sat.lp | 16 ++++++++++++++++
 3 files changed, 19 insertions(+)
 create mode 100644 pip3/q1.db
 create mode 100644 pip3/sat.lp

diff --git a/pip3/1.db b/pip3/1.db
index 4ba7a98..673f752 100644
--- a/pip3/1.db
+++ b/pip3/1.db
@@ -1,6 +1,7 @@
 left(1,wine). left(1,year). right(1,quality).
 left(2,wine). left(2,year). right(2,price).
 row(10,wine,chablis). row(10,year,1995). row(10,quality,good). row(10,price,17).
+row(9,wine,chablis). row(9,year,1995). row(9,quality,good). row(9,price,18).
 row(11,wine,chablis). row(11,year,1996). row(11,quality,excellent). row(11,price,23).
 row(12,wine,rothschild). row(12,year,1997). row(12,quality,good). row(12,price,29).
 row(13,wine,rothschild). row(13,year,1997). row(13,quality,excellent). row(13,price,29).
diff --git a/pip3/q1.db b/pip3/q1.db
new file mode 100644
index 0000000..4117a4d
--- /dev/null
+++ b/pip3/q1.db
@@ -0,0 +1,2 @@
+qrow(100,wine,chablis). qrow(100,quality,excellent). qrow(100,year,1996).
+qrow(101,wine,rothschild). qrow(101,quality,excellent).
diff --git a/pip3/sat.lp b/pip3/sat.lp
new file mode 100644
index 0000000..efde7a4
--- /dev/null
+++ b/pip3/sat.lp
@@ -0,0 +1,16 @@
+%#show qunsat/2.
+%#show qsat/1.
+%#show sat/0.
+#show unsat/0.
+%#show exist/4.
+
+qsat(Q,R) :- qrow(Q,A,V), row(R,A,V), not qunsat(Q,R).
+qunsat(Q,R) :- qrow(Q,_,_), row(R,_,_), not qsat(Q,R).
+:- qsat(Q,R), qrow(Q,A,V), not row(R,A,V).
+
+%qunsat(I) :- qrow(I,A1,V1), qrow(I,A2,V2), not exist(A1,V1,A2,V2), A1 != A2.
+
+qsat(I) :- qsat(I,_).
+%unsat() :- qrow(I,G1,G2), not qsat(I).
+:- qrow(I,G1,G2), not qsat(I).
+%sat() :- not unsat().