I have two conditions A and B in a form of "ast tree". How can I check that B is more strict than A? I.e. if B is true then A is always true.


A: x = 1 and (b = 2 or c = d)

B: y = 5 and x = 1 and (b = 2 or c = d)

Does B include A -> true

A: x = 1 and (b = 2 or c = d)

B: y = 5 and x = 1 and (b = 2 or c = d)

Does B include A -> false

This seems to be a common task for a specialist in logical math. But I have only very basic knowledge about logical arithmetics. Any articles/studies about subject appreciated.

  • $\begingroup$ An approach might be modelling $A$ and $B$ in a model checker and then verifying if the formula $B \to A$ is tautological. That being said, this is probably way too complex for someone with "only very basic knowledge about logical arithmetics"... $\endgroup$
    – dkaeae
    Dec 31 '18 at 10:44
  • 1
    $\begingroup$ What form can the conditions take? Without more information, your question can't really be answered: for example, if the only condition that's allowed is "true", then the problem is trivial; if you're allowed conditions such as "If Turing machine $M$ halts on input $x$", then the problem is undecidable. $\endgroup$ Dec 31 '18 at 21:49

If your ASTs have a small number of conditions, then you can use the following naive approach.

1) Convert your ASTs to a CSOP (Canonical Sum Of Products) expression. From your example, lets convert each condition to a boolean variable and express $A$ and $B$ as boolean expressions in the following variables

$p: (x ==1)$
$q: (y==5)$
$r: (b == 2)$
$s: (c == d)$

$ A: \space p \cdot (r + s)$
$B: p \cdot q \cdot (r + s)$

Normalising $A$ and $B$ yields
$A: p \cdot \lnot q \cdot r \cdot \lnot s + p \cdot \lnot q \cdot r \cdot s + p \cdot q \cdot r \cdot \lnot s + p \cdot q \cdot r \cdot s + p \cdot \lnot q \cdot \lnot r \cdot s + p \cdot q \cdot \lnot r \cdot s $
$B: p \cdot q \cdot r \cdot \lnot s + p \cdot q \cdot \lnot r \cdot s + p \cdot q \cdot r \cdot s $

2) Check if $ B \subseteq A$. In the above example it is true. This implies $B$ is stricter than $A$. If thought logically, all conditions in $B$ are fulfilled by $A$, but $A$ also satisfies other conditions not in $B$. Hence, $B$ is stricter compared to $A$.

Note: Expanding boolean expressions to normal forms requires exponential space. The algorithm might need some optimisation tweaks for larger expressions.

  • $\begingroup$ Your answer guided me to the right solution - thank you. But I thinking convering to Canonical Product of Sum instead, and after that's done - checking if all terms of one expressions are found in another. Else I don't see a way to "Check if B⊆A" in CSOP. $\endgroup$ Dec 31 '18 at 22:20
  • $\begingroup$ @YuriYaryshev Yes. Even CPOS can be used for the task. But use the correct one based on the expression. If an expression has $n$ variables (4 in the example) and the CSOP has $x$ product terms, then CPOS will contain $2^n-x$ sum terms. So choosing the correct Canonical form can reduce the runtime of the algorithm. $\endgroup$ Jan 1 '19 at 4:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.