From 362861de6c51c41e71f38d885033485b64207168 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 11 Nov 2022 18:27:55 +0100
Subject: [PATCH] add DPLL notebook
---
logic_programming/4_DPLL.ipynb | 991 +++++++++++++++++++++++++++++++++
1 file changed, 991 insertions(+)
create mode 100644 logic_programming/4_DPLL.ipynb
diff --git a/logic_programming/4_DPLL.ipynb b/logic_programming/4_DPLL.ipynb
new file mode 100644
index 0000000..8b7a211
--- /dev/null
+++ b/logic_programming/4_DPLL.ipynb
@@ -0,0 +1,991 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "9eb5530a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "source": [
+ "We can convert our Knights and Knaves puzzle to conjunctive normal form\n",
+ "\n",
+ "```\n",
+ "(A ⇔ B C) ∧ (B ⇔ A)\n",
+ "(A → B C) ∧ (B C → A) ∧ (B → A)∧ (A → B)\n",
+ "(A B C) ∧ ((B C) A) ∧ (B A)∧ (A B)\n",
+ "(A B C) ∧ ((B ∧ C) A) ∧ (B A)∧ (A B)\n",
+ "(A B C) ∧ (B A) ∧ (C A) ∧(B A)∧ (A B)\n",
+ "{A B C, B A, C A, B A, A B}\n",
+ "```\n",
+ "\n",
+ "Below is an encoding of the cnf as a list of lists."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "964ebd52",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ ":- discontiguous problem/3.\n",
+ ":- dynamic problem/3.\n",
+ "problem(1,'Knights & Knaves',\n",
+ " [ [neg(a),neg(b),neg(c)],\n",
+ " [pos(b),pos(a)],\n",
+ " [pos(c),pos(a)],\n",
+ " [neg(b),pos(a)],\n",
+ " [neg(a),pos(b)] ]).\n",
+ "negate(pos(A),neg(A)).\n",
+ "negate(neg(A),pos(A))."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "fc6823ad",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "source": [
+ "We can pick two clauses and resolve them as follows:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "152289b6",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mClauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+ "C1 = [neg(a),neg(b),neg(c)],\n",
+ "Lit1 = neg(a)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- problem(1,_,Clauses),\n",
+ " member(C1,Clauses), member(Lit1,C1)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "2c3dd1bf",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mClauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+ "C1 = [neg(a),neg(b),neg(c)],\n",
+ "Lit1 = neg(a),\n",
+ "Lit2 = pos(a),\n",
+ "C2 = [pos(b),pos(a)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- problem(1,_,Clauses),\n",
+ " member(C1,Clauses), member(Lit1,C1), negate(Lit1,Lit2),\n",
+ " member(C2,Clauses), member(Lit2,C2).\n",
+ "%comment."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "id": "33fc6271",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ ":- use_module(library(lists)).\n",
+ "resolve(Clause1,Clause2,Resolvent) :- \n",
+ " select(Lit1,Clause1,R1), negate(Lit1,NLit1),\n",
+ " select(NLit1,Clause2,R2),\n",
+ " append(R1,R2,Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "id": "78163b60",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mClauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+ "C1 = [neg(a),neg(b),neg(c)],\n",
+ "C2 = [pos(b),pos(a)],\n",
+ "NewClause = [neg(b),neg(c),pos(b)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- problem(1,_,Clauses),\n",
+ " member(C1,Clauses), member(C2,Clauses), \n",
+ " resolve(C1,C2,NewClause)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "9d3fbd1a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mClauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+ "NewClauses = [[neg(b),neg(c),pos(b)],[neg(a),neg(c),pos(a)],[neg(b),neg(c),pos(c)],[neg(a),neg(b),pos(a)],[neg(b),neg(c),neg(b)],[neg(a),neg(c),neg(a)],[pos(a),neg(a),neg(c)],[pos(b),neg(b),neg(c)],[pos(a),pos(a)],[pos(b),pos(b)],[pos(a),neg(a),neg(b)],[pos(c),neg(b),neg(c)],[pos(c),pos(b)],[neg(b),neg(b),neg(c)],[pos(a),pos(a)],[pos(a),neg(a)],[neg(b),pos(b)],[neg(a),neg(a),neg(c)],[pos(b),pos(b)],[pos(b),pos(c)],[pos(b),neg(b)],[neg(a),pos(a)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- problem(1,_,Clauses),\n",
+ " findall(NewClause,(member(C1,Clauses), member(C2,Clauses), \n",
+ " resolve(C1,C2,NewClause)), NewClauses)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "d32921c9",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "source": [
+ "### DPLL Algorithm\n",
+ "\n",
+ "We now present bit by bit the DPLL algorithm as a Prolog program\n",
+ "manipulating the above clause database."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "26924712",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "becomes_true(TrueLit,Clause) :-\n",
+ " member(TrueLit,Clause). "
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "17dd1525",
+ "metadata": {},
+ "source": [
+ "The above checks if making a given literal true makes the second argument, a clause, true:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "id": "7d90c4ad",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- becomes_true(pos(b),[neg(a),pos(b)])."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "id": "d4b4e71f",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- becomes_true(neg(a),[neg(a),pos(b)])."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "id": "3b9c87e4",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "simplify(TrueLit,Clause,SimplifedClause) :-\n",
+ " negate(TrueLit,FalseLit),\n",
+ " delete(Clause,FalseLit,SimplifedClause). % Resolution with TrueLit\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "id": "0abd90f6",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mR = [neg(b),neg(c)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- simplify(pos(a),[neg(a),neg(b),neg(c)],R)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "id": "cc81b404",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mR = [b,c]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- delete([a,b,c],a,R)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "53d21e85",
+ "metadata": {},
+ "source": [
+ "The above code simplifies a clause by resolution:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "id": "57df05f0",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mSC = [pos(a)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- simplify(pos(c),[pos(a),neg(c)],SC)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "id": "a36a54a4",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mSC = [pos(a),neg(c)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- simplify(pos(b),[pos(a),neg(c)],SC)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "id": "95fcf64b",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "set_literal(Lit,Clauses,NewClauses) :-\n",
+ " exclude(becomes_true(Lit),Clauses,Clauses2),\n",
+ " maplist(simplify(Lit),Clauses2,NewClauses).\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "f0a8731d",
+ "metadata": {},
+ "source": [
+ "The above code sets a given literal ```Lit``` to true by removing\n",
+ "all now redundant clauses and simplifying the remaining ones via resolution."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "id": "9c35b0b3",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mR = [[neg(b)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- exclude(becomes_true(pos(a)), [[neg(b)], [pos(a),pos(c)]],R)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "id": "8259d2d7",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mR = [[neg(b)],[pos(a)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- maplist(simplify(neg(c)), [[neg(b),pos(c)], [pos(a),pos(c)]],R)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "id": "25b19d82",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [[neg(b),neg(c)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- set_literal(pos(a),[[neg(a),neg(b),neg(c)]],Res)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "id": "5535384f",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mT = Knights & Knaves,\n",
+ "C1 = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+ "C2 = [[neg(b),neg(c)],[pos(b)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- problem(1,T,C1), set_literal(pos(a),C1,C2).\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "id": "592fcdd9",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mC1 = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+ "C2 = [[neg(b),neg(c)],[pos(b)]],\n",
+ "C3 = [[neg(c)]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- problem(1,_,C1), set_literal(pos(a),C1,C2), set_literal(pos(b),C2,C3)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "id": "b8cabba2",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "dpll(Clauses,[unit(Lit)|Stack]) :-\n",
+ " select([Lit],Clauses,Clauses2), % unit clause found\n",
+ " set_literal(Lit,Clauses2,Clauses3),\n",
+ " dpll(Clauses3,Stack).\n",
+ "dpll([],Stack) :- !, Stack=[]. % SAT\n",
+ "dpll(Clauses,[branch(Lit)|Stack]) :-\n",
+ " \\+ member([],Clauses), % no inconsistency\n",
+ " choose_literal(Clauses,Lit),\n",
+ " set_literal(Lit,Clauses,Clauses2),\n",
+ " dpll(Clauses2,Stack). \n",
+ "\n",
+ "choose_literal([ [Lit|_] | _], Lit).\n",
+ "choose_literal([ [Lit|_] | _], NegLit) :-\n",
+ " negate(Lit,NegLit).\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "id": "e369355c",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mC1 = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+ "Stack = [branch(pos(a)),unit(pos(b)),unit(neg(c))]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- problem(1,_,C1), dpll(C1,Stack).\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "id": "78764141",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "\n",
+ "test(Nr) :- problem(Nr,Str,Clauses),\n",
+ " format('Solving problem ~w : ~w~n',[Nr,Str]),\n",
+ " (dpll(Clauses,Stack)\n",
+ " -> format('SAT: Model found: ~w~n',[Stack])\n",
+ " ; format('UNSAT: no model exists',[]))."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "id": "c51455cf",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Solving problem 1 : Knights & Knaves\n",
+ "SAT: Model found: [branch(pos(a)),unit(pos(b)),unit(neg(c))]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- test(1)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "id": "b0466a5d",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "\n",
+ "\n",
+ "problem(2,'Knights & Knaves (Proof by contradiction)',\n",
+ " [ [neg(a),neg(b),neg(c)],\n",
+ " [pos(b),pos(a)],\n",
+ " [pos(c),pos(a)],\n",
+ " [neg(b),pos(a)],\n",
+ " [neg(a),pos(b)],\n",
+ " [neg(a),neg(b),pos(c)] ]). % <--- negated Query\n",
+ "problem(3,'Princess & Tiger',\n",
+ " [[pos(t1),pos(z2),neg(t1)],\n",
+ " [pos(t1),neg(z2)],\n",
+ " [neg(t1),neg(z2)],\n",
+ " [pos(t1),pos(z1),neg(t2)],\n",
+ " [pos(t2),neg(z1)],\n",
+ " [neg(t1),neg(z1)],\n",
+ " [pos(z1),pos(z2)],\n",
+ " [neg(z1),neg(z2)]])."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "id": "2df16148",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Solving problem 2 : Knights & Knaves (Proof by contradiction)\n",
+ "UNSAT: no model exists"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- test(2)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 37,
+ "id": "8d8cf76a",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Solving problem 3 : Princess & Tiger\n",
+ "SAT: Model found: [branch(neg(t1)),unit(neg(z2)),unit(pos(z1)),unit(pos(t2))]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- test(3)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "id": "31d1b945",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "problem(4,'uf-20-02',\n",
+ " [[ neg(x10) , neg(x16) , pos(x5) ] ,\n",
+ " [ pos(x16) , neg(x6) , pos(x5) ] ,\n",
+ " [ neg(x17) , neg(x14) , neg(x18) ] ,\n",
+ " [ neg(x10) , neg(x15) , pos(x19) ] ,\n",
+ " [ neg(x1) , neg(x9) , neg(x18) ] ,\n",
+ " [ pos(x3) , pos(x7) , neg(x6) ] ,\n",
+ " [ neg(x13) , pos(x1) , pos(x6) ] ,\n",
+ " [ neg(x2) , neg(x16) , neg(x20) ] ,\n",
+ " [ pos(x7) , pos(x8) , pos(x18) ] ,\n",
+ " [ neg(x7) , pos(x10) , neg(x20) ] ,\n",
+ " [ pos(x2) , neg(x14) , neg(x17) ] ,\n",
+ " [ pos(x2) , pos(x1) , pos(x19) ] ,\n",
+ " [ pos(x7) , neg(x20) , neg(x1) ] ,\n",
+ " [ neg(x11) , pos(x1) , neg(x17) ] ,\n",
+ " [ pos(x3) , neg(x12) , pos(x19) ] ,\n",
+ " [ neg(x3) , neg(x13) , pos(x6) ] ,\n",
+ " [ neg(x13) , pos(x3) , neg(x12) ] ,\n",
+ " [ pos(x5) , neg(x7) , neg(x12) ] ,\n",
+ " [ pos(x20) , pos(x8) , neg(x16) ] ,\n",
+ " [ neg(x13) , neg(x6) , pos(x19) ] ,\n",
+ " [ neg(x5) , pos(x1) , pos(x14) ] ,\n",
+ " [ pos(x9) , neg(x5) , pos(x18) ] ,\n",
+ " [ neg(x12) , neg(x17) , neg(x1) ] ,\n",
+ " [ neg(x20) , neg(x16) , pos(x19) ] ,\n",
+ " [ pos(x12) , pos(x10) , neg(x11) ] ,\n",
+ " [ pos(x6) , neg(x7) , neg(x2) ] ,\n",
+ " [ pos(x13) , neg(x10) , pos(x17) ] ,\n",
+ " [ neg(x20) , pos(x8) , neg(x16) ] ,\n",
+ " [ neg(x10) , neg(x1) , neg(x8) ] ,\n",
+ " [ neg(x7) , neg(x3) , pos(x19) ] ,\n",
+ " [ pos(x19) , neg(x1) , neg(x6) ] ,\n",
+ " [ pos(x19) , neg(x2) , pos(x13) ] ,\n",
+ " [ neg(x2) , pos(x20) , neg(x9) ] ,\n",
+ " [ neg(x8) , neg(x20) , pos(x16) ] ,\n",
+ " [ neg(x13) , neg(x1) , pos(x11) ] ,\n",
+ " [ pos(x15) , neg(x12) , neg(x6) ] ,\n",
+ " [ neg(x17) , neg(x19) , pos(x9) ] ,\n",
+ " [ pos(x19) , neg(x18) , pos(x16) ] ,\n",
+ " [ pos(x7) , neg(x8) , neg(x19) ] ,\n",
+ " [ neg(x3) , neg(x7) , neg(x1) ] ,\n",
+ " [ pos(x7) , neg(x17) , neg(x16) ] ,\n",
+ " [ neg(x2) , neg(x14) , pos(x1) ] ,\n",
+ " [ neg(x18) , neg(x10) , neg(x8) ] ,\n",
+ " [ neg(x16) , pos(x5) , pos(x8) ] ,\n",
+ " [ pos(x4) , pos(x8) , pos(x10) ] ,\n",
+ " [ neg(x20) , neg(x11) , neg(x19) ] ,\n",
+ " [ pos(x8) , neg(x16) , neg(x6) ] ,\n",
+ " [ pos(x18) , pos(x12) , pos(x8) ] ,\n",
+ " [ neg(x5) , neg(x20) , neg(x10) ] ,\n",
+ " [ pos(x16) , pos(x17) , pos(x3) ] ,\n",
+ " [ pos(x7) , neg(x1) , neg(x17) ] ,\n",
+ " [ pos(x17) , neg(x4) , pos(x7) ] ,\n",
+ " [ pos(x20) , neg(x9) , neg(x13) ] ,\n",
+ " [ pos(x13) , pos(x18) , pos(x16) ] ,\n",
+ " [ neg(x16) , neg(x6) , pos(x5) ] ,\n",
+ " [ pos(x5) , pos(x17) , pos(x7) ] ,\n",
+ " [ neg(x12) , neg(x17) , neg(x6) ] ,\n",
+ " [ neg(x20) , pos(x19) , neg(x5) ] ,\n",
+ " [ pos(x9) , neg(x19) , pos(x16) ] ,\n",
+ " [ neg(x13) , neg(x16) , pos(x11) ] ,\n",
+ " [ neg(x4) , neg(x19) , neg(x18) ] ,\n",
+ " [ neg(x13) , pos(x10) , neg(x15) ] ,\n",
+ " [ pos(x16) , neg(x7) , neg(x14) ] ,\n",
+ " [ neg(x19) , neg(x7) , neg(x18) ] ,\n",
+ " [ neg(x20) , pos(x5) , pos(x13) ] ,\n",
+ " [ pos(x12) , neg(x6) , pos(x4) ] ,\n",
+ " [ pos(x7) , pos(x9) , neg(x13) ] ,\n",
+ " [ pos(x16) , pos(x3) , pos(x7) ] ,\n",
+ " [ pos(x9) , neg(x1) , pos(x12) ] ,\n",
+ " [ neg(x3) , pos(x14) , pos(x7) ] ,\n",
+ " [ pos(x1) , pos(x15) , pos(x14) ] ,\n",
+ " [ neg(x8) , neg(x11) , pos(x18) ] ,\n",
+ " [ pos(x19) , neg(x9) , pos(x7) ] ,\n",
+ " [ neg(x10) , pos(x6) , pos(x2) ] ,\n",
+ " [ pos(x14) , pos(x18) , neg(x11) ] ,\n",
+ " [ neg(x9) , neg(x16) , pos(x14) ] ,\n",
+ " [ pos(x1) , pos(x11) , neg(x20) ] ,\n",
+ " [ pos(x11) , pos(x12) , neg(x4) ] ,\n",
+ " [ pos(x13) , neg(x11) , neg(x14) ] ,\n",
+ " [ pos(x17) , neg(x12) , pos(x9) ] ,\n",
+ " [ pos(x14) , pos(x9) , pos(x1) ] ,\n",
+ " [ pos(x8) , pos(x19) , pos(x4) ] ,\n",
+ " [ pos(x6) , neg(x13) , neg(x20) ] ,\n",
+ " [ neg(x2) , neg(x13) , pos(x11) ] ,\n",
+ " [ pos(x14) , neg(x13) , pos(x17) ] ,\n",
+ " [ pos(x9) , neg(x11) , pos(x18) ] ,\n",
+ " [ neg(x13) , neg(x6) , pos(x5) ] ,\n",
+ " [ pos(x5) , pos(x19) , neg(x18) ] ,\n",
+ " [ neg(x4) , pos(x10) , pos(x11) ] ,\n",
+ " [ neg(x18) , neg(x19) , neg(x20) ] ,\n",
+ " [ pos(x3) , neg(x9) , pos(x8) ] \n",
+ " ]).\n",
+ "problem(5,'schaltung_a1.pl',\n",
+ " [\n",
+ "%a. not_b. c. not_d. e.\n",
+ " [pos(a)], [neg(b)], [pos(c)], [neg(d)], [pos(e)],\n",
+ "% Schaltungen der ersten Ebene\n",
+ "%and11 :- a,b.\n",
+ " [pos(and11),neg(a),neg(b)], \n",
+ "%or11 :- b.\n",
+ " [pos(or11),neg(b)],\n",
+ "%or11 :- c.\n",
+ " [pos(or11),neg(b)],\n",
+ "%and12 :- c,d.\n",
+ " [pos(and12),neg(c),neg(d)], \n",
+ "%not1 :- not_e.\n",
+ " [pos(not1),pos(e)],\n",
+ "% Schaltungen der zweiten Ebene\n",
+ "%or21 :- and11.\n",
+ " [pos(or21),neg(and11)],\n",
+ "%or21 :- not1.\n",
+ " [pos(or21),neg(not1)],\n",
+ "%and2 :- or11, not1.\n",
+ " [pos(and2),neg(or11),neg(not1)], \n",
+ "%or22 :- and12.\n",
+ " [pos(or22),neg(and12)],\n",
+ "%or22 :- not1.\n",
+ " [pos(or22),neg(not1)],\n",
+ "%not2 :- e. % \\+ not1.\n",
+ " [pos(not2),neg(e)],\n",
+ "% Schaltungen der dritten Ebene\n",
+ "%and3 :- or21, and2.\n",
+ " [pos(and3),neg(or21),neg(and2)], \n",
+ "%or3 :- or22.\n",
+ " [pos(or3),neg(or22)],\n",
+ "%or3 :- not2.\n",
+ " [pos(or3),neg(not2)],\n",
+ "% Schaltungen der vierten Ebene\n",
+ "%or4 :- and3.\n",
+ " [pos(or4),neg(and3)],\n",
+ "%or4 :- or3.\n",
+ " [pos(or4),neg(or3)],\n",
+ "%and4 :- or3, not2.\n",
+ " [pos(and4),neg(or3),neg(not2)], \n",
+ "% Letzte Ebene\n",
+ "%and5 :- and4, or4.\n",
+ " [pos(and5),neg(and4),neg(or4)], \n",
+ "%output :- and5.\n",
+ " [pos(output),neg(and5)],\n",
+ "% ?- output.\n",
+ " [neg(output)]\n",
+ " ]).\n",
+ "\n",
+ "problem(6, 'doodle-wo-max1-constraint',\n",
+ " [ \n",
+ " [pos(x1),pos(x3)],\n",
+ " [neg(x3)],\n",
+ " [neg(x5)],\n",
+ " [pos(x4),pos(x5)]\n",
+ " ]).\n",
+ "problem(7, 'doodle-with-max1-constraint',\n",
+ " [ \n",
+ " [pos(x1),pos(x3)],\n",
+ " [neg(x3)],\n",
+ " [neg(x5)],\n",
+ " [pos(x4),pos(x5)],\n",
+ " \n",
+ " [neg(x1),neg(x2)], [neg(x1),neg(x3)], [neg(x1),neg(x4)],\n",
+ " [neg(x1),neg(x5)],\n",
+ " [neg(x2),neg(x3)], [neg(x2),neg(x4)],[neg(x2),neg(x5)],\n",
+ " [neg(x3),neg(x4)],[neg(x3),neg(x5)],\n",
+ " [neg(x4),neg(x5)]\n",
+ " ])."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 38,
+ "id": "c51f1ce6",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Solving problem 4 : uf-20-02\n",
+ "SAT: Model found: [branch(neg(x10)),branch(pos(x16)),branch(neg(x17)),branch(neg(x1)),branch(pos(x3)),branch(neg(x13)),branch(neg(x2)),unit(pos(x19)),branch(pos(x7)),unit(neg(x20)),unit(pos(x8)),unit(neg(x18)),unit(neg(x11)),unit(neg(x4)),branch(pos(x5)),unit(pos(x14)),unit(pos(x9)),branch(pos(x15)),branch(pos(x12))]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- test(4)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "bc767ce8",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Prolog",
+ "language": "prolog",
+ "name": "prolog_kernel"
+ },
+ "language_info": {
+ "codemirror_mode": "prolog",
+ "file_extension": ".pl",
+ "mimetype": "text/x-prolog",
+ "name": "Prolog"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
--
GitLab