C++: entailment by enumerating models

Test whether a knowledge base entails a query by checking every truth assignment.

C++

#include <iostream>

bool kb(bool a, bool b, bool c) {
  return (a || b) && (!a || c) && (!b || c);
}

template <typename Query>
bool entails(Query query) {
  for (int mask = 0; mask < 8; ++mask) {
    bool a = mask & 1, b = mask & 2, c = mask & 4;
    if (kb(a, b, c) && !query(a, b, c)) {
      return false;
    }
  }
  return true;
}

int main() {
  int models = 0;
  for (int mask = 0; mask < 8; ++mask) {
    if (kb(mask & 1, mask & 2, mask & 4)) {
      ++models;
    }
  }
  std::cout << std::boolalpha;
  std::cout << "KB models: " << models << "\n";
  std::cout << "entails C: " << entails([](bool, bool, bool c) { return c; }) << "\n";
  std::cout << "entails A: " << entails([](bool a, bool, bool) { return a; }) << "\n";
}

Output

KB models: 3
entails C: true
entails A: false

Explanation

Propositional logic describes the world with true/false symbols. A model assigns a value to each symbol. A knowledge base entails a query if the query is true in every model that satisfies the knowledge base.

The knowledge base here says: A or B, A implies C, and B implies C. Enumerating all eight models shows that exactly three satisfy it, and C is true in all three, so C is entailed. A is false in one of them, so A is not entailed. This is correct but exponential: n symbols need 2^n models.

Explore the dry run

Guided walkthroughReady

1#include <iostream>

3bool kb(bool a, bool b, bool c) {

4 return (a || b) && (!a || c) && (!b || c);

5}

7template <typename Query>

8bool entails(Query query) {

9 for (int mask = 0; mask < 8; ++mask) {

10 bool a = mask & 1, b = mask & 2, c = mask & 4;

11 if (kb(a, b, c) && !query(a, b, c)) {

12 return false;

13 }

14 }

15 return true;

16}

18int main() {

19 int models = 0;

20 for (int mask = 0; mask < 8; ++mask) {

21 if (kb(mask & 1, mask & 2, mask & 4)) {

22 ++models;

23 }

24 }

25 std::cout << std::boolalpha;

26 std::cout << "KB models: " << models << "\n";

27 std::cout << "entails C: " << entails([](bool, bool, bool c) { return c; }) << "\n";

28 std::cout << "entails A: " << entails([](bool a, bool, bool) { return a; }) << "\n";

29}

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
A or B; A implies C; B implies C. An implication p → q is written !p \|\| q.	`—`	—
A counter-model, where the KB holds but the query fails, proves the query is not entailed.	`—`	—
The satisfying models are (T,T,T), (T,F,T), and (F,T,T).	`models = 3`	KB models: 3
In the model A=false, B=true, C=true the KB holds but A fails, so A is not entailed.	`models = 3`	KB models: 3 entails C: true entails A: false

Cost and common mistakes

O(2ⁿ) models for n symbols, each checked in time linear in the formula size.

Entailment concerns all models of the KB, not just the one you have in mind.
With 30 symbols there are over a billion models. Practical systems use SAT solvers (DPLL or CDCL) instead of enumeration.

Try it yourself

Does the KB entail 'A or B'?

Reveal answer and reasoning

Yes. 'A or B' is one of its own sentences, so it holds in every model of the KB.

C++: entailment by enumerating models

Explanation

Follow the example

Cost and common mistakes

Try it yourself

Further reading