C: resolution refutation with clauses as bit masks
A clause is a disjunction of literals, such as A or not C. It can be stored as two bit masks: one with a bit for every positive literal and one with a bit for every negated literal. Two clauses resolve on a variable when one contains it positively and the other negatively. The resolvent combines the remaining literals of both.
C
#include <stdio.h>
typedef struct {
unsigned pos;
unsigned neg;
} Clause;
#define A 1u
#define B 2u
#define C 4u
static void show(Clause c) {
const char *names[] = {"A", "B", "C"};
int first = 1;
if (c.pos == 0 && c.neg == 0) {
printf("empty");
}
for (int v = 0; v < 3; v++) {
if (c.pos & (1u << v)) {
printf("%s%s", first ? "" : " v ", names[v]);
first = 0;
}
if (c.neg & (1u << v)) {
printf("%s~%s", first ? "" : " v ", names[v]);
first = 0;
}
}
}
static int same(Clause x, Clause y) {
return x.pos == y.pos && x.neg == y.neg;
}
int main(void) {
Clause clauses[64] = {
{A | B, 0},
{C, A},
{C, B},
{0, C},
};
int count = 4;
for (int i = 1; i < count; i++) {
for (int j = 0; j < i; j++) {
for (int v = 0; v < 3; v++) {
unsigned bit = 1u << v;
int opposite = ((clauses[i].pos & bit) && (clauses[j].neg & bit)) ||
((clauses[i].neg & bit) && (clauses[j].pos & bit));
if (!opposite) {
continue;
}
Clause r;
r.pos = (clauses[i].pos | clauses[j].pos) & ~bit;
r.neg = (clauses[i].neg | clauses[j].neg) & ~bit;
if (r.pos & r.neg) {
continue;
}
int seen = 0;
for (int k = 0; k < count; k++) {
if (same(clauses[k], r)) {
seen = 1;
}
}
if (seen) {
continue;
}
clauses[count++] = r;
printf("derived ");
show(r);
printf("\n");
if (r.pos == 0 && r.neg == 0) {
printf("KB entails C: 1\n");
return 0;
}
}
}
}
printf("KB entails C: 0\n");
return 0;
}