C: resolution refutation with clauses as bit masks

Represent each clause by two masks, one for positive and one for negative literals, and resolve until a contradiction appears.

#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;
}

Output

derived B v C
derived A v C
derived ~A
derived ~B
derived C
derived B
derived A
derived empty
KB entails C: 1

Explanation

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.

To prove that a knowledge base entails C, add not-C and resolve. If the empty clause appears, with both masks zero, the knowledge base together with not-C is contradictory, so C is entailed. The knowledge base is: A or B, not A or C, and not B or C. A resolvent that contains a variable both positively and negatively is a tautology and is discarded.

Explore the dry run

Guided walkthroughReady

1#include <stdio.h>

3typedef struct {

4 unsigned pos;

5 unsigned neg;

6} Clause;

8#define A 1u

9#define B 2u

10#define C 4u

12static void show(Clause c) {

13 const char *names[] = {"A", "B", "C"};

14 int first = 1;

15 if (c.pos == 0 && c.neg == 0) {

16 printf("empty");

17 }

18 for (int v = 0; v < 3; v++) {

19 if (c.pos & (1u << v)) {

20 printf("%s%s", first ? "" : " v ", names[v]);

21 first = 0;

22 }

23 if (c.neg & (1u << v)) {

24 printf("%s~%s", first ? "" : " v ", names[v]);

25 first = 0;

26 }

27 }

28}

30static int same(Clause x, Clause y) {

31 return x.pos == y.pos && x.neg == y.neg;

32}

34int main(void) {

35 Clause clauses[64] = {

36 {A | B, 0},

37 {C, A},

38 {C, B},

39 {0, C},

40 };

41 int count = 4;

43 for (int i = 1; i < count; i++) {

44 for (int j = 0; j < i; j++) {

45 for (int v = 0; v < 3; v++) {

46 unsigned bit = 1u << v;

47 int opposite = ((clauses[i].pos & bit) && (clauses[j].neg & bit)) ||

48 ((clauses[i].neg & bit) && (clauses[j].pos & bit));

49 if (!opposite) {

50 continue;

51 }

52 Clause r;

53 r.pos = (clauses[i].pos | clauses[j].pos) & ~bit;

54 r.neg = (clauses[i].neg | clauses[j].neg) & ~bit;

55 if (r.pos & r.neg) {

56 continue;

57 }

58 int seen = 0;

59 for (int k = 0; k < count; k++) {

60 if (same(clauses[k], r)) {

61 seen = 1;

62 }

63 }

64 if (seen) {

65 continue;

66 }

67 clauses[count++] = r;

68 printf("derived ");

69 show(r);

70 printf("\n");

71 if (r.pos == 0 && r.neg == 0) {

72 printf("KB entails C: 1\n");

73 return 0;

74 }

75 }

76 }

77 }

78 printf("KB entails C: 0\n");

79 return 0;

80}

Follow the example

Start to inspect the source, values, and output. These prepared steps explain the published sample; grouped loop steps describe multiple iterations.

View the complete dry-run table

Prepared trace of the published program. Some rows group repeated iterations.
What happens	State after step	Output so far
The clause A or B: two positive bits, no negative ones.	`—`	—
The negated query not-C is added as a clause.	`—`	—
The resolvent collects the other literals of both parents and drops the resolved variable.	`—`	—
A variable that appears both ways makes the clause a tautology, which is useless and skipped.	`—`	—
Each new resolvent is printed: B v C and A v C come from the knowledge base alone, ~A and ~B from resolving with the negated query, and then C, B, A, and finally the empty clause.	`—`	derived B v C derived A v C derived ~A derived ~B derived C derived B derived A derived empty
The empty clause has been derived, so the knowledge base entails C.	`—`	derived B v C derived A v C derived ~A derived ~B derived C derived B derived A derived empty KB entails C: 1

Cost and common mistakes

Exponential in the number of variables in the worst case, since there are 3ⁿ possible clauses.

The clause array holds 64 entries. A real prover must stop or grow storage before it overflows.
Resolution is complete for propositional logic, but the number of clauses can grow exponentially. Strategies such as set of support and unit preference reduce the search.
Both masks being zero means the empty clause, a contradiction, not a clause that is trivially true.

Try it yourself

What changes if the query is A?

Reveal answer and reasoning

The empty clause is never derived, because the knowledge base has a model with A false, so the loop ends with KB entails C: 0 for that query.

C: resolution refutation with clauses as bit masks

Explanation

Follow the example

Cost and common mistakes

Try it yourself

Further reading