cnf_converter.pl

%
% Copyright (C) 2021 Kian Cross
%

:- dynamic(node/4).

% Check that a node has been defined exactly once.
is_node_unique(NodeID) :-
  findall(NodeID, node(NodeID, _, _, _), Nodes),
  length(Nodes, 1).

disjoint_lists([], _).
disjoint_lists([HeadA | TailA], ListB) :-
  \+ member(HeadA, ListB),
  disjoint_lists(TailA, ListB).

validate_tree(NodeID) :- validate_tree(NodeID, [], _).

% Recursive base case (when the node ID is void, there are
% no child IDs).
validate_tree(void, _, []) :- !.

% We are trying to solve two problems
%   1) Make sure the binary tree is valid (i.e. nodes are distinct).
%   2) Make sure there are no cycles (stop infinite loops).
%
% For 2), we store a list of previously encountered nodes as we traverse
% down the tree. If a duplicate is found, it means a cycle has occurred.
%
% For 1), as we move back up the tree, we keep a list of all child nodes.
% At each node, we check that the set of child nodes from the left and right
% are disjoint (i.e. all the nodes are distinct), if they are, we merge the
% lists and go another step up the tree.
validate_tree(NodeID, TraversedNodes, ChildNodes) :-
  node(NodeID, _, LeftChild, RightChild),

  % Unfortunately we have to put a cut here to stop backtracking
  % from occurring when we validate a node with an auto_generated(_)
  % ID. Not entirely sure why this only happens with auto-generated
  % IDs, but must be something to do with the way unification works.
  % In any case, it's not a big deal, it just means you can't do a
  % query such as print_tree(X) to print every node in the knowledge-base
  % (not that there is a good reason for doing that in the first place,
  % to be fair).
  !,

  is_node_unique(NodeID),

  % Check that the node has NOT already been encountered.
  \+ member(NodeID, TraversedNodes),

  % Recursively check the left nodes, then recursively check the right
  % nodes. If these succeed, it means both the left and right side is
  % a valid binary tree.
  validate_tree(LeftChild, [NodeID | TraversedNodes], LeftChildNodes),
  validate_tree(RightChild, [NodeID | TraversedNodes], RightChildNodes),

  % Now we check that both lists are disjoint.
  disjoint_lists(LeftChildNodes, RightChildNodes),

  % If they are then we join the lists together, including the
  % ID of the current node.
  append([NodeID | LeftChildNodes], RightChildNodes, ChildNodes).

% If a unary operator is being printed (the only unary operator
% at the moment is not), then we only want to output the left child.
print_arguments(LeftChild, void) :- print_node(LeftChild), !.
print_arguments(LeftChild, RightChild) :-
  print_node(LeftChild),
  write(','),
  print_node(RightChild).

% If a node has no children then it is an atom (and therefore
% a leaf on the tree).
print_node(OpProp, void, void) :- write(OpProp), !.
print_node(OpProp, LeftChild, RightChild) :-
  write(OpProp),
  write('('),
  print_arguments(LeftChild, RightChild),
  write(')').

% Expand a node ID to a node with all
% arguments.
print_node(NodeID) :-
  node(NodeID, OpProp, LeftChild, RightChild),

  % We can cut here, as we only want the first node with a given ID
  % (they should be distinct in the knowledge-base anyway).
  !,
  print_node(OpProp, LeftChild, RightChild).

% Print the tree, performing validation first.
print_tree(NodeID) :-
  validate_tree(NodeID),
  print_node(NodeID).

unique_id(NewID) :- unique_id(NewID, 0).

% If no node exists with the current ID, then
% we can use it.
unique_id(autogenerated(Counter), Counter) :- \+ node(autogenerated(Counter), _, _, _), !.

% Otherwise we need to increment the counter, then recursively
% call the goal again.
unique_id(NewID, Counter) :-
  IncrementedCounter is Counter + 1,
  unique_id(NewID, IncrementedCounter).

% Unlike before, we do not just have to worry about automatically
% generating internal nodes, Now, because of distributivity, we need
% to be able to duplicate leaf nodes. This causes a problem. With
% internal nodes, we just used the IDs of the children to construct
% an ID for the new node. However, leave nodes don't have children.
% So we have to generate a new unique ID.
autogenerated_id(void, void, NewID) :- unique_id(NewID), !.
autogenerated_id(LeftChild, RightChild, autogenerated(LeftChild, RightChild)).

% Duplicates a node and all of it's children. Here is how it works:
%   1) Recurse all the way down to the leaf nodes. For these, nodes,
%      generate a unique ID.
%
%   2) Then, as we work our way back up the tree, set the IDs for the
%      internal nodes to autogenerated(LeftChild, RightChild). i.e. we
%      use the IDs of the children to construct an ID for the current node.
deep_duplicate_node(void, void).
deep_duplicate_node(NodeID, NewID) :-
  node(NodeID, OpProp, LeftChild, RightChild),
  deep_duplicate_node(LeftChild, NewLeftChildID),
  deep_duplicate_node(RightChild, NewRightChildID),
  autogenerated_id(NewLeftChildID, NewRightChildID, NewID),
  asserta(node(NewID, OpProp, NewLeftChildID, NewRightChildID)).

% Used by DeMorgan law, so that we can use one rule
% for both AND and OR.
and_or_map(and, or).
and_or_map(or, and).

% The rules below are fairly self explanatory.

demorgan(NodeID) :-
  node(NodeID, not, LeftChild, void),
  node(LeftChild, Op, P, Q),
  and_or_map(Op, FlippedOp),
  autogenerated_id(Q, void, NewNodeID),
  retract(node(NodeID, not, LeftChild, void)),
  retract(node(LeftChild, Op, P, Q)),
  asserta(node(NodeID, FlippedOp, LeftChild, NewNodeID)),
  asserta(node(LeftChild, not, P, void)),
  asserta(node(NewNodeID, not, Q, void)).

double_negation_elimination(NodeID) :-
  node(NodeID, not, LeftChild, void),
  node(LeftChild, not, LeftSubChild, void),
  node(LeftSubChild, P, PLeft, PRight),
  retract(node(NodeID, not, LeftChild, void)),
  retract(node(LeftChild, not, LeftSubChild, void)),
  asserta(node(NodeID, P, PLeft, PRight)).

implication_elimination(NodeID) :-
  node(NodeID, implies, LeftChild, RightChild),
  autogenerated_id(LeftChild, void, NewNodeID),
  retract(node(NodeID, implies, LeftChild, RightChild)),
  asserta(node(NodeID, or, NewNodeID, RightChild)),
  asserta(node(NewNodeID, not, LeftChild, void)).

% converting OR(AND(P, Q), R) to AND(OR(P, R), OR(Q, R)).
or_over_and_distributivity(NodeID) :-
  node(NodeID, or, LeftChild, R),
  node(LeftChild, and, P, Q),
  deep_duplicate_node(R, NewR),
  autogenerated_id(Q, NewR, NewOrID),
  retract(node(NodeID, or, LeftChild, R)),
  retract(node(LeftChild, and, P, Q)),
  asserta(node(NodeID, and, LeftChild, NewOrID)),
  asserta(node(LeftChild, or, P, R)),
  asserta(node(NewOrID, or, Q, NewR)).

% converting OR(P, AND(Q, R) to AND(OR(P, Q), OR(P, R)).
or_over_and_distributivity(NodeID) :-
  node(NodeID, or, R, RightChild),
  node(RightChild, and, P, Q),
  deep_duplicate_node(R, NewR),
  autogenerated_id(Q, NewR, NewOrID),
  retract(node(NodeID, or, R, RightChild)),
  retract(node(RightChild, and, P, Q)),
  asserta(node(NodeID, and, NewOrID, RightChild)),
  asserta(node(NewOrID, or, NewR, P)),
  asserta(node(RightChild, or, R, Q)).

% applies a rule to all nodes on a tree. We have to fail so that
% backtracking happens automatically. Start at the top and work
% down (pre-order traversal).
apply_rule_to_tree_pre(void, _) :- !, fail.
apply_rule_to_tree_pre(NodeID, Rule) :- call_with_args(Rule, NodeID), fail.

% Recurse down the left sub-tree.
apply_rule_to_tree_pre(NodeID, Rule) :-
  node(NodeID, _, LeftChild, _),
  apply_rule_to_tree_pre(LeftChild, Rule).

% Recurse down the left right-tree.
apply_rule_to_tree_pre(NodeID, Rule) :-
  node(NodeID, _, _, RightChild),
  apply_rule_to_tree_pre(RightChild, Rule).


% Apply a rule to the tree, but start at leaves and move
% upwards (i.e. post-order traversal).
apply_rule_to_tree_post(void, _) :- !, fail.

% Recurse down the left sub-tree.
apply_rule_to_tree_post(NodeID, Rule) :-
  node(NodeID, _, LeftChild, _),
  apply_rule_to_tree_post(LeftChild, Rule).

% Recurse down the left right-tree.
apply_rule_to_tree_post(NodeID, Rule) :-
  node(NodeID, _, _, RightChild),
  apply_rule_to_tree_post(RightChild, Rule).

apply_rule_to_tree_post(NodeID, Rule) :- call_with_args(Rule, NodeID), fail.


% We need to keep reapplying negation elimination and
% De Morgan's law to a node until there is nothing left
% to eliminate.
negation_normal_form_node(NodeID) :-
  double_negation_elimination(NodeID), 
  negation_normal_form_node(NodeID).

negation_normal_form_node(NodeID) :-
  demorgan(NodeID),
  negation_normal_form_node(NodeID).

% Apply the above to every node in the tree. Doing so will
% put the tree into negation normal form.
negation_normal_form(NodeID) :-
  % Note that we apply the rules as we move into the tree,
  % because we are 'pushing' the NOTs inwards.
  apply_rule_to_tree_pre(NodeID, negation_normal_form_node).

move_ands_out(NodeID) :-
  or_over_and_distributivity(NodeID),

  % Keep bubbling ANDs up this part of the sub-tree
  % until there are no more 'distributivities'. At
  % this point the goal will fail, and we will move
  % up to the next level of the tree.
  apply_rule_to_tree_post(NodeID, move_ands_out).

% We have to fail so that backtracking happens automatically.
conjunctive_normal_form(NodeID) :- apply_rule_to_tree_pre(NodeID, implication_elimination), fail.
conjunctive_normal_form(NodeID) :- negation_normal_form(NodeID), fail.

% Apply distributivity to a node. Keep repeating until
% we can not perform distributivity on a node any more
% (i.e. we have moved the ANDs as high up as possible in
% the tree). Once this has happened, we move one level
% up the tree and repeat the same to the node, again
% moving ANDs as high up as possible. Eventually we will
% reach the root node, at which point we have 'bubbled'
% the ANDs all the way to the top of the tree. Note in
% particular when applying these rules we do it from
% the leaves of the tree upwards. This is in contrast to
% negation_normal_form/1 which applies rules from the
% roots down to the leaves. Because we are 'bubbling'
% the ANDs out from the centre of the formula, we want
% to start at the leaves and work outwards.
conjunctive_normal_form(NodeID) :- apply_rule_to_tree_post(NodeID, move_ands_out), fail.