Prev: 3x10^10 cm/sec uniquely linked to the end of Finiteness at 10^28?? #564 Correcting Math
Next: Mathematical Logic and the Strengthened Liar's Paradox
From: RussellE on 3 Apr 2010 20:21
I want to OR two 2CNF expressions.
I know DNF to CNF conversions can produce
an exponetial number of CNF clauses.
Even so, I would like to know how
large a CNF can be assuming it is
the union of two 2CNF expressions.

Some examples:
First formula is (a+b) and second formula is (c+d):
(a+b) + (c+d) = (a+b+c+d)

(a+b)&(c+d) + (e+f)&(g+h) =
(a+b+e+f)&(c+d+e+f)&(a+b+g+h)&(c+d+g+h)

I think I can say no clause will be larger
than a 4-clause. I can convert 4-clauses
into 3-clauses by adding variables.

Is there any "good" way to OR two 2CNF's?
My method is pretty much brute force.

This problem arises from my study of partitions.
I think this is a generalized form of resolution.

Assume I have this 3SAT instance:
(a+b+c)&(~a+d+e)

Create a partition of one variable.
Partition: (a)
Clauses in partition: (a+b+c) & (~a+d+e)

There are two possible assignments for
the clauses in this partition: a and ~a
(a)&(d+e) + (~a)&(b+c)

We can remove (a) and (~a): (b+c) + (d+e)
We now have the problem I described above.

(b+c) + (d+e) = (b+c+d+e)

Notice, this is the same result we would
get from resolving (a+b+c) & (~a+d+e).

I could have partitioned on variable b.
(b) + (~b)&(a+c)

This becomes a tautology when we remove
(b) and (~b). Because (b) is a pure literal,
we can always assume there is a satisfying
assignment where (b) is true,
if there is a satisfying assignment.

Paritions can have any number of variables.

3SAT instance:
(a+b+c) & (~a+c+~d) & (~b+c+~e) & (~b+~d+~e)

Partition: ab
Clauses: (a+b+c)(~a+c+~d)(~b+c+~e)(~b+~d+~e)
Formula:

( (a) & (b) & (c+~d) & (c+~e) & (~d+~e) ) +
( (~a) & (b) & (c+~e) & (~d+~e) ) +
( (a) & (~b) & (c+~d) ) +
( (~a) & (~b) & (c) )

Removing variables a and b:

(c+~d)&(c+~e)&(~d+~e) +
(c+~e)&(~d+~e) +
(c+~d) + (c)
=
(c+~d+~e)

Any satisfying assignment of (c+~d+~e)
is consistent with some satisfying assignment
of the instance, if the instance has a satisfying
assignment.

For example, (~c) & (d) & (~e) satisfies (c+~d+~e).
Reducing
(a+b+c) & (~a+c+~d) & (~b+c+~e) & (~b+~d+~e)
we get:
(a+b) & (~a) = (~a) & (b).

(~a) & (b) & (~c) & (d) & (~e)

(a+B+c)&(~A+c+~d)&(~b+c+~E)&(~b+~d+~E)


Is this type of resolution equivalent to known
forms of resolution?

It seems I can extend the "pure literal rule"
to any partition which reduces to a tautology.

Split the 3SAT instance into two groups:
Clauses in the partition and clauses not
in the partition.

If the reduced formula for the partition
is a tautology, then, for any satisfying
assignment of the clauses not in the partition,
there exists an assignment of variables
in the partition which satisfy the
remaining clauses in the partition.


Russell
- 2 many 2 count
From: RussellE on 4 Apr 2010 17:24
This is a more complex example of the
"Pure Partition" rule:

Given a 3SAT instance:
(a+b+~c) & (~a+b+d) & (~a+c+~d) & (~b+c+~e) & (~b+~d+~e)

Partition on variables a and b:
ab: (c+~d) & (c+~e) & (~d+~e)
~ab: (c+~e) & (~d+~e)
a~b: (d) & (c+~d)
~a~b: (~c)

Reduced partition formula:
(c+~d) & (c+~e) & (~d+~e) +
(c+~e) & (~d+~e) +
(d) & (c+~d) +
(~c)

=

(~c+c+~d) & (~c+c+~e) & (~c+~d+~e) +
(~c+c+~e) & (~c+~d+~e) +
(~c+d) & (~c+c+~d)

=

(~c+~d+~e) + (~c+d) =
(~c+d+~d+~e) = True

Since the partition formula is a tautology,
there exists a satisfying assignment of
variables a and b for any assignment of
the non-index variables, c, d, and e.

For example, assume c, d, and e are all false.

Reduce:
(~a+b)

Assume c, d, and e are all true:

Reduce:
(a+b) & (~b) = (a) & (~b)


Russell
- 2 many 2 count

 | 
Pages: 1
Prev: 3x10^10 cm/sec uniquely linked to the end of Finiteness at 10^28?? #564 Correcting Math
Next: Mathematical Logic and the Strengthened Liar's Paradox