Thanks for the idea of this problem to our colleague Vadim Pelyushenko!
There is a Boolean Logic, you know :) Logic formulas include variables, which only could be false or true
and operations between them. In this problem we have description of some logic function, built as a chain
of operations on few input variables - and want to transform it to more plain form, namely
full disjunctive normal form.
Input consists of set of rules, each taking only 2 variables and naming result as some new variable.
Syntax for the rule is Z := X op Y where Z is result variable, X and Y could be prepended with
negation operator, and the operation (op) itself could be one of:
and - conjunction (both operands need to be true)or - disjunction (at least one needs to be true)-> - implication (if X is true, then Y needs too)eq - equality (operands should be equal)xor - exclusive disjunction (operands should be different)All variables are denoted with small latin letters (a ... z). Of them first four (a, b, c, d) are input
variables, while others appear as results in rules. There are no loops in rule definitions (no feedbacks). One
of variables (latest of letters) is considered output.
Full Disjunctive Normal Form consists of disjunction (or) of several parts, where every of those parts is
conjunction (and) of all input variables with different set of negations applied to them each time. For
example implication (mentioned above) is represented in FDNF as following:
x&y | ~x&y | ~x&~y
However, while x&y | ~x is also DNF, it is not "full" (rather, contracted by combining two parts of
full form).
In the answer we use &, | signs instead and, or respectively - simply for compactness.
Input gives number of rules and the name of output variable.
Then rules follow, one per line.
Answer should provide full disjunctive normal form of four variables. Order and spaces do not matter.
Example:
input:
8 l
l := k and f
k := f -> j
e := d xor ~c
f := ~e xor a
g := ~e -> ~b
h := d eq g
i := h -> b
j := b or i
answer:
a&b&c&d | a&b&~c&~d | a&~b&~c&~d | ~a&b&~c&d | ~a&b&c&~d | ~a&~b&c&~d