Not a direct answer to your question but are you aware of library(clpb): CLP(B): Constraint Logic Programming over Boolean Variables?

```
?- use_module(library(clpb)).
true.
?- sat(A * ~B * C).
A = C, C = 1,
B = 0.
?- sat(A * ~A).
false.
```

If you question is for a homework exercise, then at least you can use this to cross check your work.

References:

Computability and Logic 5th Edition

by George S. Boolos, John P. Burgess and Richard C. Jeffrey

(PDF) (WorldCat)

Machine Program for Theorem-Proving

Automated Reasoning: satisfiability Coursera video

Satisfiability (Wikipedia)

From: Computability and Logic 5th Edition

A set of sentences L is unsatisfiable if no interpretation makes L true (and is satisfiable if some interpretation does).

DPLL (Wikipedia) (Wikipedia Talk)

Unit propagation (Wikipedia)

DPLL(T ) as a goal-directed proof-search mechanism

Examples using SWI-Prolog clpb to demonstrate satisfiable.

P

```
?- sat(P).
P = 1.
```

~P

```
?- sat(~P).
P = 0.
```

P AND Q

```
?- sat(P*Q).
P = Q, Q = 1
```

P |
Q |
P AND Q |

0 |
0 |
0 |

0 |
1 |
0 |

1 |
0 |
0 |

1 |
1 |
1 |

P OR Q

NB clpb will simplify a formula, however for these examples the values are needed so labeling must be used for this example.

```
?- sat(P+Q),labeling([P,Q]).
P = 0, Q = 1 ;
P = 1, Q = 0 ;
P = Q, Q = 1
```

P |
Q |
P OR Q |

0 |
0 |
0 |

0 |
1 |
1 |

1 |
0 |
1 |

1 |
1 |
1 |

Note: clpb needs a space with some operators (I don’t know the exact rules for such), e.g.

```
?- sat(P*~P).
ERROR: Syntax error: Operator expected
ERROR: sat(
ERROR: ** here **
ERROR: P*~P) .
```

```
?- sat(P * ~P).
false.
```

P |
NOT P |
P AND NOT P |

0 |
1 |
0 |

1 |
0 |
0 |

Since `P AND NOT P`

is always false, it is not satisfiable.

Example from Wikipedia Unit Propagation

NB This is in CNF - a conjunction of one or more clauses, where a clause is a disjunction of literals;

(A OR B) AND (NOT A OR C) AND (NOT C OR D) AND A

```
?- sat((A + B) * (~A + C) * (~C + D) * A).
A = C, C = D, D = 1,
sat(B=:=B).
?- sat((A + B) * (~A + C) * (~C + D) * A), labeling([A,B,C,D]).
A = C, C = D, D = 1, B = 0 ;
A = B, B = C, C = D, D = 1.
```

A |
B |
C |
D |
A OR B |
NOT A OR C |
NOT C OR D |
A |
(A OR B) AND (NOT A OR C) AND (NOT C OR D) AND A |

0 |
0 |
0 |
0 |
0 |
1 |
1 |
0 |
0 |

0 |
0 |
0 |
1 |
0 |
1 |
1 |
0 |
0 |

0 |
0 |
1 |
0 |
0 |
1 |
0 |
0 |
0 |

0 |
0 |
1 |
1 |
0 |
1 |
1 |
0 |
0 |

0 |
1 |
0 |
0 |
1 |
1 |
1 |
0 |
0 |

0 |
1 |
0 |
1 |
1 |
1 |
1 |
0 |
0 |

0 |
1 |
1 |
0 |
1 |
1 |
0 |
0 |
0 |

0 |
1 |
1 |
1 |
1 |
1 |
1 |
0 |
0 |

1 |
0 |
0 |
0 |
1 |
0 |
1 |
1 |
0 |

1 |
0 |
0 |
1 |
1 |
0 |
1 |
1 |
0 |

1 |
0 |
1 |
0 |
1 |
1 |
0 |
1 |
0 |

1 |
0 |
1 |
1 |
1 |
1 |
1 |
1 |
1 |

1 |
1 |
0 |
0 |
1 |
0 |
1 |
1 |
0 |

1 |
1 |
0 |
1 |
1 |
0 |
1 |
1 |
0 |

1 |
1 |
1 |
0 |
1 |
1 |
0 |
1 |
0 |

1 |
1 |
1 |
1 |
1 |
1 |
1 |
1 |
1 |

Note: The clpb source code does not have any test cases, or at least that I could find, so here are some for demonstration purposes.

```
:- begin_tests(clpb).
% Logical not
test(001) :-
findall([P],(sat(~P),labeling([P])),Solutions),
assertion( Solutions == [[0]] ).
% Logical and
test(002) :-
findall([P,Q],(sat(P * Q),labeling([P,Q])),Solutions),
assertion( Solutions == [[1,1]] ).
% Logical or
test(003) :-
findall([P,Q],(sat(P + Q),labeling([P,Q])),Solutions),
assertion( Solutions == [[0,1],[1,0],[1,1]] ).
% Logical exclusive or
test(004) :-
findall([P,Q],(sat(P # Q),labeling([P,Q])),Solutions),
assertion( Solutions == [[0,1],[1,0]] ).
% http://profs.sci.univr.it/~farinelli/courses/ar/slides/DPLL.pdf
% Example 1 - Showing how to test a satisfication that fails using the Prolog unit test ability to check for failure.
test(101,[fail]) :-
sat((P + Q + ~R) * (P + ~Q) * ~P * R * U).
% Example 1 - Showing how to test a satisfication that fails using labeling/1 with assertion/1 for failure.
test(102) :-
findall([P,Q,R,U],(sat((P + Q + ~R) * (P + ~Q) * ~P * R * U),labeling([P,Q,R,U])),Solutions),
assertion( Solutions == [] ).
% Example 2
test(103) :-
findall([P,Q,R],(sat((P + Q) * ~Q * (~P + Q + ~R)),labeling([P,Q,R])),Solutions),
assertion( Solutions == [[1,0,0]] ).
% Example 3
test(104) :-
findall([P,Q,R],(sat((P + Q) * (P + ~Q) * (~P + Q) * (~P + ~R)),labeling([P,Q,R])),Solutions),
assertion( Solutions == [[1,1,0]] ).
% Example 4
test(105) :-
findall([P,Q,R],(sat((P + ~Q) * (~P + R) * Q),labeling([P,Q,R])),Solutions),
assertion( Solutions == [[1,1,1]] ).
% Exercise 1
test(106) :-
findall([P,Q,R],(sat((P + Q) * (~P + Q) * (~R + ~Q) * (R + ~Q)),labeling([P,Q,R])),Solutions),
assertion( Solutions == [] ).
% Exercise 2
test(107) :-
findall([P,Q,R],(sat((P + Q + R) * (~P + ~Q + ~R) * (~P + Q + R) * (~Q + R) * (Q + ~R)),labeling([P,Q,R])),Solutions),
assertion( Solutions == [[0,1,1]] ).
% Exercise 3
test(108) :-
findall([P,Q,R],(sat((~Q + P) * (~P + ~Q) * (Q + R) * (~Q + ~R) * (~P + ~R) * (P + ~R)),labeling([P,Q,R])),Solutions),
assertion( Solutions == [] ).
:- end_tests(clpb).
```