1

The partial ordering rules of constraints are defined as:
[temp.constr.order#1]

A constraint P subsumes a constraint Q if and only if, for every disjunctive clause Pi in the disjunctive normal form of P, Pi subsumes every conjunctive clause Qj in the conjunctive normal form of Q, where

  • a disjunctive clause Pi subsumes a conjunctive clause Qj if and only if there exists an atomic constraint Pia in Pi for which there exists an atomic constraint Qjb in Qj such that Pia subsumes Qjb, and
  • an atomic constraint A subsumes another atomic constraint B if and only if A and B are identical using the rules described in [temp.constr.atomic].

I don't know how to get the disjunctive and conjunctive normal forms of a given constraint. Moreover, I have some confusion about the second bullet.

Question 1:

Given a constraint named P with the form A ∧ B and another constraint named Q with the form A where A and B are both atomic constraints. For constraint P what's the disjunctive normal form of it? Whereas, what's the conjunctive and disjunctive normal form of Q?

Question 2:

Is that Pi and Qj is taken from the clauses of the corresponding positions of their disjunctive /conjunctive normal form? Especially, how to understand the sentence if and only if there exists an atomic constraint Pia in Pi for which there exists an atomic constraint Qjb in Qj such that Pia subsumes Qjb? How to interpret the case that Qi has an extra atomic constraint that Pi does not have? Does that P subsumes Q? Could you give an exposition process to interpret why does A ∧ B subsume A?

xmh0511
  • 7,010
  • 1
  • 9
  • 36

1 Answers1

1

Both A ∧ B and A are already in disjunctive normal form and conjunctive normal form.

In this case, there is one disjunctive clause in P, and one conjunctive clause in Q.

You then check if any subclause of P0 (A ∧ B) subsumes any subclause of Q0 (A), which it does (A subsumes A).

Caleth
  • 52,200
  • 2
  • 44
  • 75
  • How to get DNF or CNF? If `P0(A)` while `Q0(A V B)`, Does that P0 subsume Q0? – xmh0511 Mar 11 '21 at 13:04
  • You have to substitute clauses until you have a disjunction of conjunctions (for dnf) or a conjunction of disjunctions (for cnf). `((a ^ b) v c) ^ d` is an example of something you'd have to mess with, as is `!(a ^ b)` – Caleth Mar 11 '21 at 13:06
  • It may be clearer if I overbracket your example: `P = ((A ∧ B))`; `P0 = (A ∧ B)`; `P00 = A`, `P01 = B`. `Q = ((A))`; `Q0 = (A)`; `Q00 = A`. – Caleth Mar 11 '21 at 13:12
  • For the second bullet, Does that mean merely exists Pia that can identity to Qib, then Pi will subsume Qi? Such as `P0(A)` and Q0(A V B)? P0 will subsume Q0? – xmh0511 Mar 11 '21 at 13:12
  • Yes, because `P00` subsumes `Q00` – Caleth Mar 11 '21 at 13:15
  • Isn't `A V B` a disjunction clause of Q where its CNF were `(A V B) ∧ B`? That is Q0 would be `A V B` while P0 were `A` – xmh0511 Mar 11 '21 at 13:17
  • Let us [continue this discussion in chat](https://chat.stackoverflow.com/rooms/229769/discussion-between-caleth-and-jack-x). – Caleth Mar 11 '21 at 13:18