C++ · Course navigation

C++: entailment by enumerating models

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

On this page

Before you start

C++ lambdas and templates.

Test whether a knowledge base entails a query by checking every truth assignment.
Predict the sample output and explain the state changes.
Complete the practice task and check the boundary cases.

The concept

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.

Code example

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

Example details

Follow the code

Open the walkthrough to inspect the example one step at a time.

Show guided walkthrough

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

Behind the scenes

How C++ processes this code

The C++ compiler produces a native executable. Execution enters main, where objects and function calls perform the work.

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.