"One can encode a clause as a set of literals, and one can encode the CNF as a set of clauses.\n",
"Implicitly, the literals in clause are disjoined, while all the clauses in a CNF are conjoined.\n",
"In Prolog, we can represent sets using lists.\n",
"Below is an encoding of the CNF as a list of lists."
"Below is an encoding of the CNF as a list of lists.\n",
"For example, the clause ```¬A ∨ ¬B ∨ ¬C``` is represented as the list ```[neg(a),neg(b),neg(c)]```.\n",
"Every literal is of either the form ```neg(p)``` or ```pos(p)``` with ```p``` being a proposition."
]
},
{
"cell_type": "code",
"execution_count": 3,
"execution_count": 4,
"id": "964ebd52",
"metadata": {
"vscode": {
...
...
@@ -56,6 +58,39 @@
"negate(neg(A),pos(A))."
]
},
{
"cell_type": "markdown",
"id": "a4dc903e",
"metadata": {},
"source": [
"We can negate literals as follows:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "26e0221b",
"metadata": {
"vscode": {
"languageId": "prolog"
}
},
"outputs": [
{
"data": {
"text/plain": [
"\u001b[1mNA = neg(a),\n",
"NB = pos(b)"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"?- negate(pos(a),NA), negate(neg(b),NB)."
]
},
{
"cell_type": "markdown",
"id": "fc6823ad",
...
...
@@ -65,7 +100,8 @@
}
},
"source": [
"We can pick two clauses and resolve them as follows:"
"We now show to perform resolution of two clauses.\n",
"First we can pick two clauses simply using ```member```:"
]
},
{
...
...
@@ -95,6 +131,14 @@
" member(C1,Clauses), member(Lit1,C1)."
]
},
{
"cell_type": "markdown",
"id": "68fd6059",
"metadata": {},
"source": [
"We can now pick matching literals with opposing polarity as follows:"
]
},
{
"cell_type": "code",
"execution_count": 5,
...
...
@@ -126,9 +170,17 @@
"%comment."
]
},
{
"cell_type": "markdown",
"id": "07785e91",
"metadata": {},
"source": [
"We can now implement resolution of two particular clauses as follows:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"execution_count": 8,
"id": "33fc6271",
"metadata": {
"vscode": {
...
...
@@ -144,6 +196,126 @@
" append(R1,R2,Resolvent)."
]
},
{
"cell_type": "markdown",
"id": "1d426bb1",
"metadata": {},
"source": [
"The above predicate uses the predicate ```select/3``` from ```library(lists)```, which can be used to select an element from a list and returns a modified list with the element removed:"
"As you can see, the number of new clauses can grow considerably when applying resolution.\n",
"Below we study the DPLL algorithm to check satisfiability of a formula in CNF, using a simple form of resolution (where one clause is a single literal and the other clauses comes from the CNF of the problem)."
]
},
{
...
...
@@ -212,12 +407,15 @@
"### DPLL Algorithm\n",
"\n",
"We now present bit by bit the DPLL algorithm as a Prolog program\n",
"manipulating the above clause database."
"manipulating the above clause database.\n",
"\n",
"The algorithm works by selecting a literal and then making it true and checking whether this leads to a solution.\n",
"If not, the algorithm backtracks and makes the negated version of the literal true and tries to find a solution."
]
},
{
"cell_type": "code",
"execution_count": 9,
"execution_count": 23,
"id": "26924712",
"metadata": {
"vscode": {
...
...
@@ -235,7 +433,7 @@
"id": "17dd1525",
"metadata": {},
"source": [
"The above checks if making a given literal true makes the second argument, a clause, true:"
"The above checks if making a given literal true makes the second argument, a clause, true (i.e., the clause is satisfied):"
]
},
{
...
...
@@ -286,9 +484,18 @@
"?- becomes_true(neg(a),[neg(a),pos(b)])."
]
},
{
"cell_type": "markdown",
"id": "62e13b8d",
"metadata": {},
"source": [
"The code below simplifies a clause given a literal ```TrueLit``` that has just become true.\n",
"This is done using resolution:"
]
},
{
"cell_type": "code",
"execution_count": 12,
"execution_count": 24,
"id": "3b9c87e4",
"metadata": {
"vscode": {
...
...
@@ -299,12 +506,20 @@
"source": [
"simplify(TrueLit,Clause,SimplifedClause) :-\n",
" negate(TrueLit,FalseLit),\n",
" delete(Clause,FalseLit,SimplifedClause). % Resolution with TrueLit\n"
" delete(Clause,FalseLit,SimplifedClause). % Resolution with TrueLit if possible\n"
]
},
{
"cell_type": "markdown",
"id": "e8cee74e",
"metadata": {},
"source": [
"The code uses the ```delete/3``` predicate from ```library(lists)```. Unlike select it also succeeds when the element is not in the list:"
]
},
{
"cell_type": "code",
"execution_count": 13,
"execution_count": 19,
"id": "0abd90f6",
"metadata": {
"vscode": {
...
...
@@ -315,7 +530,7 @@
{
"data": {
"text/plain": [
"\u001b[1mR = [neg(b),neg(c)]"
"\u001b[1mR = [a,b,c]"
]
},
"metadata": {},
...
...
@@ -323,7 +538,7 @@
}
],
"source": [
"?- simplify(pos(a),[neg(a),neg(b),neg(c)],R)."
"?- delete([a,b,c],d,R)."
]
},
{
...
...
@@ -382,6 +597,14 @@
"?- simplify(pos(c),[pos(a),neg(c)],SC)."
]
},
{
"cell_type": "markdown",
"id": "4c3eae55",
"metadata": {},
"source": [
"If no resolution is possible the clause is returned unchanged:"
]
},
{
"cell_type": "code",
"execution_count": 16,
...
...
@@ -406,9 +629,19 @@
"?- simplify(pos(b),[pos(a),neg(c)],SC)."
]
},
{
"cell_type": "markdown",
"id": "441c4145",
"metadata": {},
"source": [
"We can now define the whole procedure to set a literal ```Lit``` to true (```Clauses|{Lit}```) by\n",
"- removing all clauses which have become true (and no longer need to be checked)\n",
"- simplifying the remaining clauses with resolution if possible."
]
},
{
"cell_type": "code",
"execution_count": 17,
"execution_count": 25,
"id": "95fcf64b",
"metadata": {
"vscode": {
...
...
@@ -427,13 +660,12 @@
"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."
"The predicate ```exclude/3``` from ```library(lists)``` is a higher-order predicate. It maps its first argument (a predicate) over the second argument (a list) and excludes all elements where the predicate succeeds."
"```exclude``` will perform these two calls and hence remove the second clause and keep the first one:"
]
},
{
"cell_type": "code",
"execution_count": 27,
"id": "56175b0d",
"metadata": {
"vscode": {
"languageId": "prolog"
}
},
"outputs": [
{
"data": {
"text/plain": [
"\u001b[1;31mfalse"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
"\u001b[1mtrue"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"?- becomes_true(pos(a),[neg(b)]).\n",
"?- becomes_true(pos(a),[pos(a),pos(c)])."
]
},
{
"cell_type": "markdown",
"id": "52063b72",
"metadata": {},
"source": [
"The predicate ```maplist/3``` from ```library(lists)``` is another higher-order predicate. It maps its first argument (a predicate) over the elements in the second and third arguments (both lists)."
We can now implement resolution of two particular clauses as follows:
%% Cell type:code id:33fc6271 tags:
``` prolog
:-use_module(library(lists)).
resolve(Clause1,Clause2,Resolvent):-
select(Lit1,Clause1,R1),negate(Lit1,NLit1),
select(NLit1,Clause2,R2),
append(R1,R2,Resolvent).
```
%% Cell type:markdown id:1d426bb1 tags:
The above predicate uses the predicate ```select/3``` from ```library(lists)```, which can be used to select an element from a list and returns a modified list with the element removed:
As you can see, the number of new clauses can grow considerably when applying resolution.
Below we study the DPLL algorithm to check satisfiability of a formula in CNF, using a simple form of resolution (where one clause is a single literal and the other clauses comes from the CNF of the problem).
%% Cell type:markdown id:d32921c9 tags:
### DPLL Algorithm
We now present bit by bit the DPLL algorithm as a Prolog program
manipulating the above clause database.
The algorithm works by selecting a literal and then making it true and checking whether this leads to a solution.
If not, the algorithm backtracks and makes the negated version of the literal true and tries to find a solution.
%% Cell type:code id:26924712 tags:
``` prolog
becomes_true(TrueLit,Clause):-
member(TrueLit,Clause).
```
%% Cell type:markdown id:17dd1525 tags:
The above checks if making a given literal true makes the second argument, a clause, true:
The above checks if making a given literal true makes the second argument, a clause, true (i.e., the clause is satisfied):
%% Cell type:code id:7d90c4ad tags:
``` prolog
?-becomes_true(pos(b),[neg(a),pos(b)]).
```
%% Output
%% Cell type:code id:d4b4e71f tags:
``` prolog
?-becomes_true(neg(a),[neg(a),pos(b)]).
```
%% Output
%% Cell type:markdown id:62e13b8d tags:
The code below simplifies a clause given a literal ```TrueLit``` that has just become true.
This is done using resolution:
%% Cell type:code id:3b9c87e4 tags:
``` prolog
simplify(TrueLit,Clause,SimplifedClause):-
negate(TrueLit,FalseLit),
delete(Clause,FalseLit,SimplifedClause).% Resolution with TrueLit
delete(Clause,FalseLit,SimplifedClause).% Resolution with TrueLit if possible
```
%% Cell type:markdown id:e8cee74e tags:
The code uses the ```delete/3``` predicate from ```library(lists)```. Unlike select it also succeeds when the element is not in the list:
%% Cell type:code id:0abd90f6 tags:
``` prolog
?-simplify(pos(a),[neg(a),neg(b),neg(c)],R).
?-delete([a,b,c],d,R).
```
%% Output
%% Cell type:code id:cc81b404 tags:
``` prolog
?-delete([a,b,c],a,R).
```
%% Output
%% Cell type:markdown id:53d21e85 tags:
The above code simplifies a clause by resolution:
%% Cell type:code id:57df05f0 tags:
``` prolog
?-simplify(pos(c),[pos(a),neg(c)],SC).
```
%% Output
%% Cell type:markdown id:4c3eae55 tags:
If no resolution is possible the clause is returned unchanged:
%% Cell type:code id:a36a54a4 tags:
``` prolog
?-simplify(pos(b),[pos(a),neg(c)],SC).
```
%% Output
%% Cell type:markdown id:441c4145 tags:
We can now define the whole procedure to set a literal ```Lit``` to true (```Clauses|{Lit}```) by
- removing all clauses which have become true (and no longer need to be checked)
- simplifying the remaining clauses with resolution if possible.
%% Cell type:code id:95fcf64b tags:
``` prolog
set_literal(Lit,Clauses,NewClauses):-
exclude(becomes_true(Lit),Clauses,Clauses2),
maplist(simplify(Lit),Clauses2,NewClauses).
```
%% Cell type:markdown id:f0a8731d tags:
The above code sets a given literal ```Lit``` to true by removing
all now redundant clauses and simplifying the remaining ones via resolution.
The predicate ```exclude/3``` from ```library(lists)``` is a higher-order predicate. It maps its first argument (a predicate) over the second argument (a list) and excludes all elements where the predicate succeeds.
```exclude``` will perform these two calls and hence remove the second clause and keep the first one:
%% Cell type:code id:56175b0d tags:
``` prolog
?- becomes_true(pos(a),[neg(b)]).
?- becomes_true(pos(a),[pos(a),pos(c)]).
```
%% Output
%% Cell type:markdown id:52063b72 tags:
The predicate ```maplist/3``` from ```library(lists)``` is another higher-order predicate. It maps its first argument (a predicate) over the elements in the second and third arguments (both lists).
Michael Leuschel <leuschel@uni-duesseldorf.de>