3SAT is Almost 2SAT

From: Russell Easterly (logiclab_at_comcast.net)
Date: 02/05/05 

Date: Fri, 4 Feb 2005 21:32:39 -0800

This may all be circular, but here goes.

Any Boolean function can be converted
to 3SAT. 3SAT can be converted to
exclusive 3SAT (X3SAT)

Any X3SAT instance can be converted
to what I am calling Almost 2SAT (A2SAT).
A2SAT is actually 3SAT with a lot of binary clauses.

Converting X3SAT to A2SAT:
Consider the X3SAT clause: (a,b,u)
where u is a unique literal.

(a,b,u) -> (~a OR ~b)

The value of u can be calculated from this formula:

u = (~a AND ~b)

Consider the X3SAT clause (a,b,c):

(a,b,c) ->
(~a OR ~b) AND (~a OR ~c) AND (~b OR ~c) AND (a OR b OR c)

This shows that any X3SAT can be
converted to A2SAT. 3SAT can be converted
to A2SAT by first converting to X3SAT
and then converting to A2SAT.

3SAT -> X3SAT
(a OR b OR c) -> (~a,u,x)(~b,v,y)(~c,w,z)(x,y,z)
(u, v, and w are unique)

X3SAT -> A2SAT
(~a,u,x)(~b,v,y)(~c,w,z)(x,y,z) ->
(a OR ~x)(b OR ~y)(c OR ~z)(~x OR ~y)(~x OR ~z)(~y OR ~z)(x OR y OR z)

3SAT -> A2SAT
(a OR b OR c) ->
(a OR ~x)(b OR ~y)(c OR ~z)(~x OR ~y)(~x OR ~z)(~y OR ~z)(x OR y OR z)

Why would we want to convert a 3SAT instance to a bigger
3SAT instance with more clauses and variables?

One possible reason is to do a quick and dirty check for unsatisfiable
instances.
Let F() be a A2SAT instance and let F() = F2() AND F3() where
F2() are the binary clauses in F() and F3() are the 3-clauses.
A solution for F2() can be found in linear time (with respect to the
clauses).
If F2() has no solution then F() has no solution.

Another reason to use this conversion is that some SAT solvers will
use 2SAT to help solve a 3SAT problem.
BINSat is an example of such a solver.

I don't have access to a BINSat solver, but I would be very
interested in whether this conversion (as a pre-process)
makes a 3SAT instance easier to solve.

Russell
- 2 many 2 count

Relevant Pages

  • 3SAT is Almost 2SAT
    ... Any X3SAT instance can be converted ... A2SAT is actually 3SAT with a lot of binary clauses. ... Converting X3SAT to A2SAT: ...
    (sci.logic)
  • 3SAT is Almost 2SAT
    ... Any X3SAT instance can be converted ... A2SAT is actually 3SAT with a lot of binary clauses. ... Converting X3SAT to A2SAT: ...
    (sci.math)
  • Re: WHERE statement conditions
    ... Here is a quick trick for converting IF-THEN-ELSE procedural code in ... The CASE expression evaluates the WHEN clauses in order and returns ...
    (microsoft.public.sqlserver.programming)