C++: backward chaining from a goal

Prove a goal by finding a rule that concludes it and then proving that rule's conditions.

C++

#include <iostream>
#include <map>
#include <set>
#include <string>
#include <vector>

std::set<std::string> facts = {"rain", "cold"};
std::map<std::string, std::vector<std::string>> rules = {
    {"wet", {"rain"}},
    {"ice", {"wet", "cold"}},
    {"slippery", {"ice"}},
};

bool prove(const std::string& goal, int depth) {
  std::cout << std::string(depth * 2, ' ') << "goal " << goal;
  if (facts.count(goal)) {
    std::cout << " -> fact\n";
    return true;
  }
  auto rule = rules.find(goal);
  if (rule == rules.end()) {
    std::cout << " -> no rule\n";
    return false;
  }
  std::cout << "\n";
  for (const std::string& condition : rule->second) {
    if (!prove(condition, depth + 1)) {
      return false;
    }
  }
  return true;
}

int main() {
  std::cout << (prove("slippery", 0) ? "proved" : "not proved") << "\n";
  std::cout << (prove("sunny", 0) ? "proved" : "not proved") << "\n";
}

Output

goal slippery
  goal ice
    goal wet
      goal rain -> fact
    goal cold -> fact
proved
goal sunny -> no rule
not proved

Explanation

Backward chaining is goal-directed reasoning. To prove a goal, the system first checks whether it is a known fact. If not, it looks for a rule whose conclusion is that goal and tries to prove every condition of the rule, recursively. This is how Prolog answers queries.

The program stores facts and rules and prints each goal it tries with indentation showing the depth of the recursion. Unlike forward chaining, it only works on rules relevant to the question. A rule set with a cycle, such as a depends on b and b depends on a, would recurse forever unless visited goals are tracked.

Explore the dry run

Guided walkthroughReady

1#include <iostream>

2#include <map>

3#include <set>

4#include <string>

5#include <vector>

7std::set<std::string> facts = {"rain", "cold"};

8std::map<std::string, std::vector<std::string>> rules = {

9 {"wet", {"rain"}},

10 {"ice", {"wet", "cold"}},

11 {"slippery", {"ice"}},

12};

14bool prove(const std::string& goal, int depth) {

15 std::cout << std::string(depth * 2, ' ') << "goal " << goal;

16 if (facts.count(goal)) {

17 std::cout << " -> fact\n";

18 return true;

19 }

20 auto rule = rules.find(goal);

21 if (rule == rules.end()) {

22 std::cout << " -> no rule\n";

23 return false;

24 }

25 std::cout << "\n";

26 for (const std::string& condition : rule->second) {

27 if (!prove(condition, depth + 1)) {

28 return false;

29 }

30 }

31 return true;

32}

34int main() {

35 std::cout << (prove("slippery", 0) ? "proved" : "not proved") << "\n";

36 std::cout << (prove("sunny", 0) ? "proved" : "not proved") << "\n";

37}

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 known fact proves the goal immediately.	`—`	—
Otherwise look for a rule that concludes this goal.	`—`	—
Every condition of the rule must be proved; one failure fails the rule.	`slippery ⇐ ice ⇐ wet, cold ⇐ rain`	—
The indentation shows the proof tree: only rules related to the goal were used.	`slippery ⇐ ice ⇐ wet, cold ⇐ rain`	goal slippery goal ice goal wet goal rain -> fact goal cold -> fact proved
sunny is neither a fact nor the conclusion of any rule, so the proof fails.	`slippery ⇐ ice ⇐ wet, cold ⇐ rain`	goal slippery goal ice goal wet goal rain -> fact goal cold -> fact proved goal sunny -> no rule not proved

Cost and common mistakes

In the worst case exponential; here each goal is proved at most once, so the work is linear in the rules used.

A cyclic rule set causes infinite recursion. Track the goals being proved to detect loops.
This map holds one rule per conclusion. Real systems allow several rules for the same conclusion and try each alternative (backtracking).

Try it yourself

What would the output be for goal 'wet'?

Reveal answer and reasoning

'goal wet' followed by an indented 'goal rain -> fact', then 'proved'.

C++: backward chaining from a goal

Explanation

Follow the example

Cost and common mistakes

Try it yourself

Further reading