Number of 2SATs in 3SAT

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

Date: Fri, 25 Feb 2005 14:57:44 -0800

Number of 2SATs in 3SAT

Let V be a set of Boolean variables
and let F be a set of 3-clauses of
variables in V.

Let X be a subset of V such that
every clause in F contains at
least one variable in X.
Let x = |X| be the size of X.

If a variable in a 3-clause is given
an assignment then either the 3-clause
is satisfied or the 3-clause can be
reduced to a 2-clause.

F can be reduced to 2SAT by giving
an assignment to all the variables in X.
There are 2^x different 2SAT instances
that F can be reduced into.
If any of these 2SAT instances
has a solution then F is solvable, else
F has no solution.

Define x to be that smallest number of
variables one can randomly choose from V
to put in X and be sure every clause in F
contains a member of X.

There is a simple proof that x <= (n-2).
(where n is the number of variables in V)

Assume we have chosen a set of variables
to put in X such that there is exactly
one clause in F that doesn't contain
a variable in X.

This clause contains three variables not
in X and we only have to choose one variable
to satisfy this clause. This shows there
are at least two variables in V that don't
have to be in X.

x also depends on the number of clauses in F
and the clause to variable ratio.
I don't have a closed form formula for x, yet,
but x is fairly simple to calculate for
a given number of clauses and variables.
Hopefully, someone on sci.math can come up
with a closed formula for x.

Let V have n variables and F have m clauses.
Assume that no clause in F contains
the same variable more than once.

At least one variable in V must be in
at least 3*m/n clauses of F.

Let n=10 and m=40.

3*40/10 = 12 clauses removed by first variable
3*(40-12)/(10-1) =
3*28/9 = 10 clauses removed by second variable
3*18/8 = 7
3*11/7 = 5
3*6/6 = 3
3*3/5 = 2
3*1/4 = 1 clause removed by seventh variable

x=7 for n=10, m=40

The formula for x seems to be a little chaotic.
It looks like x depends on the clause to variable
ratio, be it also tends to grow as m grows.
For example, assuming n = m, x = n/2 for small
values of n and m, but x grows slowly for
larger values of n and m.

Russell
- 2 many 2 count

Relevant Pages

  • Re: DELETING 100 million from a table weekly SQl SERVER 2000
    ... > The delete statement's where clause has the conditions for A, ... using a predicate that can be satisfied by the clustered index, ... > 1) Does this setting ROWCOUNT first sort the table and then delete? ... it just deletes the first N rows it finds that satisfy the ...
    (microsoft.public.sqlserver.tools)
  • Number of 2SATs in 3SAT
    ... to put in X and be sure every clause in F ... to satisfy this clause. ... and the clause to variable ratio. ... I don't have a closed form formula for x, yet, ...
    (comp.theory)
  • Number of 2SATs in 3SAT
    ... to put in X and be sure every clause in F ... to satisfy this clause. ... and the clause to variable ratio. ... I don't have a closed form formula for x, yet, ...
    (sci.math)
  • RE: AS400/DB2 Problem with Group By clause
    ... In order to solve this I've arbitrarily added the max function to the other fields just to satisfy the query syntax. ... > Set adoRS = adoCD.Execute ... > Adding the GROUP BY clause: ...
    (microsoft.public.vb.database.ado)