Строительный блокнот  Automata methods and madness 

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 [ 145 ] 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175

a) F is in CNF, and consists of at most n clauses.

b) F is constructible from E in time at most c\E\.

c) A truth assignment T for E malces E true if and only if there exists an extension S of T that makes F true.

BASIS: If E consists of one or two symbols, then it is a literal. A literal is a clause, so E is already in CNF.

INDUCTION: Assume that every expression shorter than E can be converted to a product of clauses, and that this conversion takes at most cn time on an expression of length n. There are two cases, depending on the top-level operator oiE.

Case 1: E = El Л E2. By the inductive hypothesis, there are expressions Fy and F2 derived from Ei and E2, respectively, in CNF. All and only the satisfying assignments for Ej can be extended to a satisfying assignment for Fi, and similarly for E2 and 2- Without loss of generality, we may assume that the variables of Fi and F2 are disjoint, except for those variables that appear in E; i.e., if we have to introduce variables into Fi and/or F2, use distinct variables.

Let F = Fi A F2. Evidently Fi л F2 is a CNF expression if F] and F2 are. We must show that a truth assignment T for E can be extended to a satisfying assignment for F if and only if T satisfies E.

(If) Suppose T satisfies E. Let Tj be T restricted so it applies only to the variables that appear in Ei, and let T2 be the same for £2- Then by the inductive hypothesis, Ti and T2 can be extended to assignments Si and S2 that satisfy Fi and F2, respectively. Let S agree with Si and S2 on each of the variables they define. Note that, since the only variables Fi and F2 have in common aie the rariables of E, and 5j and S2 must agree on those variables if both are defined, it is always possible to construct S. But S is then an extension of Г that satisfies F.

(Only-if) Conversely, suppose that T has an extension S that satisfies F. Let Ti (resp., T2) be T restricted to the variables of Ei (resp., £2). Let S restricted to the variables of Fi (resp., F2) be Si (resp., 52). Then Si is an extension of T], and S2 is an extension of Tj. Because F is the AND of Fi and F2, it must be that Si satisfies Fi, and 2 satisfies F. By the inductive hypothesis, Ti (resp., T2) must satisfy Ei (resp., E2). Thus, T satisfies E.

Case 2: E = Ei У E2. As in case 1, we invoke the inductive hypothesis to assert that there are CNF expressions Fi and F2 with the properties:

1. A truth assignment for Ei (resp., E2) satisfies Ei (resp £2), if and only if it can be extended to a satisfying assignment for Fi (resp., F2).

2. The variables of £1 and £2 are disjoint, except for those variables that appear in £.



3. Fi and F-z are in CNF.

We cannot simply take the OR of Fi and F2 to construct the desired F, because the resulting expression would not be in CNF. However, a more complicated construction, which takes advantage of the fact that we only want to preserve satisfiability, rather than equivalence, will work. Suppose

Fi = gi A 92 A A gp

and Fi - h\ A h2 A A hq, where the ps and /Is are clauses. Introduce a new variable y, and let

= (1/ + 9i) Л (y + 52) Л Л (y + Pj,) Л (17 + hi) A{y + h2)A---A{y + hg)

We must prove that a truth assignment T for E satisfies E if and only if T can be extended to a truth assignment S that satisfies F.

(Only-if) Assume T satisfies E. As in Case 1, let Ti (resp., T2) be T restricted to the variables of Ei (resp., E2). Since E - Ej V E2, either Г satisfies Ei or T satisfies E2. Let us assume T satisfies Ei. Then Ti, which is T restricted to the variables of Fi, can be extended to Sj, which satisfies Ft Construct an extension S for Г, as follows; S will satisfy the expression F defined above:

1. For all variables a; in F S{x) - Si{x).

2. S{y) = 0. This choice makes all the clauses of F that are derived from F2 true.

3. For all variables x that are in F2 but not in Fi, S{x) is T{x) if the latter is defined, and otherwise may be 0 or 1, abribtrarily.

Then S makes all the clauses derived from the ps true because of rule 1. 5 makes all the clauses derived from the hs true by rule 2 - the truth assignment for y. Thus, 5 satisfies F.

If T does not satisfy Ei, but satisfies F2, then the argument is the same, except S{y) - 1 in rule 2. Also, S{x) must agree with S2{x) whenever 52(x) is defined, but S{x) for variables appearing only in Si is arbitrary. We conclude that S satisfies F in this case also.

(If) Suppose that truth assignment T for F is extended to truth assignment S for F, and S satisfies F. There are two cases, depending on what truth-value is assigned to y. First suppose that 5(y) - 0, Then all the clauses of F derived from the hs are true. However, у is no help for the clauses of the form {y + gi) that are derived from the ps, which means that S must make true each of the pjs themselves; in essence, S makes Fi true.

More precisely, let Si be S restricted to the variables of Fi. Then Si satisfies Fi. By the inductive hypothesis, Ti, which is T restricted to the variables of Fi, must satisfy Ei. The reason is that is an extension of Ti. Since Ti satisfies Fi, T must satisfy E, which is Fi V F2.



We must also consider the case that S{y) - 1, but this case is symmetric to what we have just seen, and we leave it to the reader. We conclude that T satisfies E whenever S satisfies F.

Now, we must show that the time to construct F from E is at most quadratic, in n, the length of E. Regardless of which case applies, the splitting apart of E into El and E-2, and construction of F from Fi and Fa each take time that is linear in the size of E. Let dn be an upper bound on the time to construct Ei and E2 from E plus the time to construct F from Fi and Fn, in either case 1 or case 2. Then there is a recurrence equation for T(n), the time to construct F from any E of length n; its form is:

T(l) T(2) < e for some constant e

T{n) <dn + cmaxo<t<n-i {T{i) + T(n ~ 1 - i)) for n > 3

Where с is a constant as yet to be determined, such that we can show T{n) < cn. The basis rule for T(l) and T(2) simply says that if £ is a single symbol or a pair of symbols, then we need no recursion because E can only be a single literal, and the entire process takes some amount of time e. The recursive rule uses the fact that if E is composed of subexpressions Fj and £2 connected by an operator л or V, and £1 is of length i, then £a is of length n - i - I. Moreover, the entire conversion of £ to F consists of the two simple steps - changing £ to £1 and £2 and changing Fi and F2 to £ - that we know take time at most dn, plus the two recursive conversions of £1 to Fi and £2 to Fg.

We need to show by induction on n that there is a constant с such that for all n, T(n) < cn.

BASIS: For n - 1, we just need to pick с at least as large as e,

INDUCTION: Assume the statement for lengths less than n. Then T(i) < сг and T{n-i-l) <c{n-i - 1). Thus,

T{i) + T(n - г - 1) < - 2i(n - 0 - 2(n - i) + 1 (lO.lJ

Since n > 3, and 0 < i < u - 1, 2i{n - i) is at least n, and 2(n - i) is at least 2, Thus, the right side of (10.1) is less than -n, for any г in the allowed range. The recursive rule in the definition of T{n) thus says T{n) < dn + cn - cn. If we pick c> d, we may infer that T(n) < cn holds for n, which concludes the induction. Thus, the construction of F from £ takes time O(n). □

Example 10.14: Let us show how the construction of Theorem 10.13 applies to a simple expression: £ - xj/ + x{y + 2). Figure 10.7 shows the parse of this expression. Attached to each node is the CNF expression constructed for the expression represented by that node.

The leaves correspond to the literals, and for each literal, the CNF expression is one clause consisting of that literal alone. For instance, we see that the leaf labeled у has an associated CNF expression (y), The parentheses are



1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 [ 145 ] 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175