Prev: comp.theory charter
Next: COMSOC-2008, updated Call for Papers
From: reasterly on 23 Apr 2008 01:32
I'm interested in seeing how much of a 3-SAT instance
can be converted into 2-SAT.

I have been reading research that says the "critical point"
for 2+p-SAT is about 2/5.

The p in 2+p-SAT is the percentage of the clauses in
the instance that are 3-clauses, the rest being 2-clauses.

The "critical point" is where the difficulty of solving the instance
goes from roughly linear, for 2-SAT, to exponential, like 3-SAT.
For this problem, the critical point is determined experimentally
using "random" instances.

I am curious if there is any theoretical attempts to determine
the critical point of 2+p-SAT.

I have previously posted some 3SAT to 2+p-SAT conversions.
This new one adds fewer clauses and variables than
previous conversions.

Start with a conversion from 3SAT to 1 in 3 SAT(X3SAT):

(a,b,c) is defined as choose exactly 1 of a, b, or c.
(a+b+c) is defined as the 3-SAT clause (a OR b OR c)

(a+b+c) ->
(x1,x2,x3)&(~a,x1,u1)&(~b,x2,u2)&(~c,x3,u3)
where u1, u2, and u3 are unique literals.

A literal is unique if it appears in exactly one clause
and its negation doesn't appear in any clause.

An unique literal can be removed from an X3SAT clause
and the X3-clause replaced with a 2-clause:

If u is unique:
(a,b,u) -> (~a+~b) where u=~a&~b

Replacing u1, u2, and u3 with 2-clauses:

(a+b+c) ->
(x1,x2,x3)&(a+~x1)&(b+~x2)&(c+~x3)

Notice that x1,x2, and x3 are almost unique.
They appear in only two clause, an X3-clause
(unnegated) and a 2-clause (negated).

We can remove x1 as long as we replace ~x1.
Negating x1=~x2&~x3 gives us ~x1=(x2+x3).

Removing x1, replacing (x1,x2,x3) with (~x2+~x3),
and replacing ~x1 with (x2+x3):

(a+b+c) ->
(~x2+~x3)&(a+(x2+x3))&(b+~x2)&(c+~x3)

Renaming variables:

(a+b+c) ->
(a+x1+x2)&(b+~x1)&(c+~x2)&(~x1+~x2)

When a 3SAT instance is converted to 2+p-SAT
using this method, p=1/4. Of course, the resulting
2+p-SAT instance is far from random.


Russell
- 2 many 2 count
 | 
Pages: 1
Prev: comp.theory charter
Next: COMSOC-2008, updated Call for Papers