2

Assume that we are given a logical expression like $A$ and ($B$ or $C$) and $D$. The total evaluation of the expression is false and we know the value of each operand $(A,B,C,D)$. I need to develop an algorithm which get a logical expression and the value of operands, and determine which operands make the expression false.

for example:

logical expression $\text{exp} = A$ and (not $B$)

logical operands: $A$ : true , $B$ : true

The algorithm determines that $B$ violates the expression.

  • 2
    Have you considered a truth table? – abiessu Jun 25 '15 at 02:38
  • @abiessu He said develop an algorithm. Thus, by suggesting truth tables, since they usually involve calculating all sub-formulas before the calculating an expression. If the expression is not a tautology that doesn't sound very efficient (though correct). – Doug Spoonwood Jun 25 '15 at 03:24
  • First you are going have to give a precise specification of your algorithm. The description you have given is unclear. E.g., $(A \Rightarrow B) \land (B \Rightarrow A)$ is true iff the values assigned to $A$ and $B$ are the same. If $A$ is true and $B$ is false, how is your algorithm supposed to decide which of them is "violating" the condition that they are the same. – Rob Arthan Jun 25 '15 at 10:08

1 Answers1

1
  1. Determine the number of variables in the expression and store this in something like "num_vars".
  2. Find all bit_strings (sequences of '0s' and '1s') which have the same length as num_vars. Store each of these in an ordered structure.
  3. Number, or order the variables in the logical expression. For instance, A is always the first variable, B always the second, and so on.
  4. Set the current bit string as the 0th element of the bit_string ordered structure.
  5. For all variables in the expression, replace the nth_variable of a clone of the expression with the nth_element of the current bit string. E. G. if the current bit string is 0011, then replace the variable 'A' with '0', 'B' with '0', 'C' with '1', and 'D' with '0'.
  6. Calculate whether the resulting formula (with just connectives and '0s' and '1s') is a tautology or not. If it is not a tautology, then halt. The expression is not a tautology. Otherwise continue.
  7. If the current bit string is not the last bit_string in the bit_string list, then set the current bit_string to the successor of the bit_string (bit_string + 1), and then goto 5. Otherwise, halt, the formula is a tautology.

Example: CaCbc

Three variables (step 1).

['000', '001', '010', '011', '100', '101', '110', '111'] (step 2)

a - 0, b - 1, c - 2 (step 3)

current_bit_string = 0 (step 4)

C0C00 (step 5)

1 (step 6) and thus we continue

current_bit_string = 1 (step 7)

C0C01 (step 5)

1 (step 6)

current_bit_string = 2 (step 7)

C0C10 (step 5)

1 (step 6)

current_bit_string = 3 (step 7)

C0C11 (step 5)

1 (step 6)

current_bit_string = 4 (step 7)

C1C00 (step 5)

1 (step 6)

current_bit_string = 5 (step 7)

C1C01 (step 5)

1 (step 6)

current_bit_string = 6 (step 7)

C1C10 (step 5)

0 Halt this is not a tautology. (step 6)

Note step 2. The bit_strings can appear in any order so long as we have all of them. If we have some more knowledge about when a formula is not a tautology, we might thus make the algorithm more efficient using that knowledge, by generating all bit strings and re-ordering them according to when when an expression is not a tautology. Or just by using that knowledge in another way.

For instance, if the expression only has conditionals, and we're working in prefix notation, then if an expression is not a tautology, then the formula is not a tautology when at some instance where the last variable instantiates as 0. Thus, we might re-order the ordered structure of bit_strings as follows such that those bit_strings where '0' is the last element come first.

['000', '010', '100', '110', ...]

Thus, we end up as more likely to find those cases where a formula is not a tautology more quickly. And actually, in this case where we only have conditional symbols, we do NOT need to check any of the cases where the last element of the bit_string equals '1'. We only need to check the cases where the last element of the bit_string equals '0'.