After an intuitive description, we next introduce the basic CDC constraints in Nc for clause c ≡ p
∗
r ∨ p
∗
s ∨ p
∗ t in φ.

We begin with the constraints involving the four auxiliary 'pier' spatial variables w c 0
, wc rs, wc st and w c 1
. As shown in Figure 8, these variables are interpreted as rectangles that are bridged by the frames f 0 r
, f 0 s
, and f 0 t
.

k (w c 0 , wref ), k (w c 1 , wref ), (37) o ⊗ f(w c 0 , fr), (38) o ⊗ eq(fr, wc rs), o ⊗ eq(w c rs, fs), if p ∗ r = pr, o ⊗ fi(f¬r, wc rs), o ⊗ eq(w c rs, fs), if p ∗ r = ¬pr, o ⊗ eq(fs, wc st), o ⊗ eq(w c st, ft), if p ∗ s = ps, o ⊗ fi(f¬s, wc st), o ⊗ eq(w c st, ft), if p ∗ s = ¬ps, o ⊗ fi(ft, wc1 ), if p ∗ t = pt, o ⊗ fi(f¬t, wc1 ), if p ∗ t = ¬pt.
$$(38)$$
(39)  $\binom{40}{41}$  (41)  ... 
Note the k constraint and RA constraints o ⊗ f, o ⊗ eq, o ⊗ fi in the above equations are shorthands of the basic CDC constraints that entail them (cf. Example 1). The first equation (Eq. 37) requires that w c 0 and w c 1 are of the same height as the reference spatial variable wref . The second equation (Eq. 38) specifies the RA relation between w c 0 and fr.

The third equation (Eq. 39) specifies that w c rs is of the same height as the inner frame fi of ui. The position of w c rs, however, depends on the sign of literal p
∗ r
. If p
∗ r is positive, then we require w c rs to bridge the gap between fr and fs; otherwise, we require w c rs to bridge the gap between f¬r and fs. The constraints involving w c st, specified in Eq. 40, are similar. The last equation (Eq. 41) specifies that ft overlaps w c 1 if p
∗
t is positive, and f¬t overlaps w c 1 otherwise.

We illustrate the construction of the above constraints with an example.

Example 4. Consider the clause c = pr ∨ ¬ps ∨ pt. Figure 11 illustrates the configuration of variables w c 0
, wc rs, wc st, wc1 in the frames of ur, us and ut. The network Nc specifies that o ⊗ f(w c 0
, fr); o ⊗ eq(fr, wc rs), o ⊗ eq(w c rs, fs); o ⊗ fi(f¬s, wc st), o ⊗ eq(w c st, ft); and o ⊗ fi(ft, wc1
).

Figure 12 examines the possible position of u
∗
r = ur and u
∗
s = u¬s. If ur is horizontally instantiated, then the gap between ur and u¬s is certainly bridged by w c rs (Figure 12(a)); if ur is vertically instantiated, then it is possible to make ur 'thin' enough so that the gap between ur and u¬s is maintained (Figure 12(b)). Similar results hold for u¬s
(see Figure 12(c)(d) for illustration). In case ur, u¬s, and ut are all horizontally instantiated, then there is no gap between any consecutive two of the seven regions. Otherwise, if any of ur, u¬s, and utis vertically instantiated, then it is possible to maintain some gap.