System for determining propositional logic theorems by applying values and rules to triplets that are generated from boolean formula

An apparatus for determining, in tautology checks, whether or not all possible assignments of truth values 0 and 1 to variables in a boolean formula render the boolean formula true, said apparatus comprising:

• a sequence unit which is responsive to information received from all remaining connected units to determine which state in a series of stages shall be carried out;
• a generator which is connected to the sequence unit via communication buses and which is operative to generate triplets from the boolean formula;
• a permanent unit including an addressable memory facility for storing at each memory address words which correspond to variables in a triplet;
• a plurality of evaluators, the number of evaluators corresponding to the number of combinations of constant values to which a tuple of test-variables can be instantiated, each evaluator dedicated to processing a corresponding one of the combinations of constant values to which a tuple of test variables can be instantiated, each said evaluator including an addressable memory matrix for storing at each memory address words which correspond to variables in a triplet, the addressable memory matrix comprising three substantially identical addressable memory units, each said memory unit having a data input port coupled to receive a corresponding one of the variables in a triplet, an address input port coupled to an address source that is common to all said three memory units, and a white control input coupled through a selector to receive a write control signal derived from a comparison of a comparand and a word contained at an address of the memory unit;
• and
• an analyzer, connected to said permanent unit and to said evaluators, and operative to generate pairs of addresses corresponding to variables for evaluation, wherein said addresses are sent to all evaluators and to the permanent unit via a bus, whereafter analysis of a pair is carried out in said evaluators and said permanent unit to produce results that are sent to said analyzer.