Prev: ICNAAM 2010 Mini-Symposium on Computational Bioimaging and Visualization
Next: CFP with Extended Deadline of Mar. 21, 2010: The 2010 International Conference on Foundations of Computer Science (FCS'10), USA, July 2010
From: RussellE on 9 Mar 2010 23:37
I describe a method of classifying clauses
in a 3SAT instance. One type of clause is
always satisfiable in polynomial steps.
Two other types of clauses are solvable
in polynomial steps if certain conditions
are met.

Index set: a maximal set of independent clauses
Index clause: a clause in the index set
Index variable: a variable which appears in an index clause
Non-Index variable: a variable that is not an index variable

Two clauses are independent if they share
no variables in common. A set of independent
clauses is maximal if no more clauses in
the instance can be added to the set.

There is a simple algorithm for creating a
maximal independent set of clauses:

Choose a clause from the instance.
Add this clause to the index set.
Remove all clauses having a variable
in common with this clause.

Repeat this process on the remaining clauses
until all clauses are removed.

Every clause in a 3SAT instance can be
uniquely classified with respect to an index set.

Type 1: Clauses with 3 variables in common
with an index clause.

Type 2: Clauses with 2 variables in common
with an index clause and 1 non-index variable.

Type 3: Clauses with 1 variable in common
with an index clause and 2 non-index variables.

Type 4: Clauses with 1 variable in common
with 2 different index clauses and 1 non-index
variable.

Type 5: Clauses with 2 variables in common
with one index clause and 1 variable in
common with another index clause.

Type 6: Clauses with 1 variable in common
with 3 different index clauses.


I will refer to index clause families.
An index clause family is the index clause
and all type 1, 2, and 3 clauses which
share variables in common with the index clause.

An index clause family has no more than
seven satisfying assignments.

Type 1 clauses can be solved in a
polynomial number of steps:

1) Find all satisfying assignments
for the type 1 clauses in each
index clause family.

2) An index clause family with eight
type 1 clauses in unsatisfiable making
the entire instance unsatisfiable.

3) Choose a satisfying assignment from
each index clause family.

The satisfying assignments for type 1
clauses in an index clause family form
the "base formula".

Type 1 clauses: (a+b+c)(~a+b+~c)(a+~b+~c)
Base formula: a~b~c + ~ab~c + ab~c + ~a~bc + abc

Each satisfying assignment either satisfies
a type 2 clause or makes the type 2 clause
a unit clause. The unit clause forces the
assignment of a non-index variable.

We can "extend" the base fomula with unit
propagation of the type 2 clauses.
Note, unit propogation may remove terms
from the base formula.

Type 2 clauses: (~a+~b+x)(a+c+y)(~a+b+x)

Extended formula:
a~b~c(x) + ~ab~c(y) + ab~c(x) + ~a~bc() + abc(x)

We can reduce this formula by removing the
base variables a,b, and c. These variables
don't appear in any other type 1 or 2 clauses.

Reduced formula:
x + y + x + T + x = T

Notice ~a~bc does not force the assignment
of any non-index varibles. This means the
reduced formula is a tautology. We can
choose the assignment ~a~bc regardless
of the assignments of the non-index
variables.

All type 1 and type 2 clauses can be
solved in polynomial steps if the
reduced formula for each index clause
family has two or fewer variables.

Assume the reduced formula for every
index clause family is a tautology.

1) Choose an arbitrary assignment for
the non-index variables.

2) For each index clause family,
choose a satisfying assignment from
the extended formula consistent with
the assignment of non-index variables.
There must be such an assignment if
the reduced formula is a tautology.

Assume the reduced formula for one
or more index clause familys has
two variables.

The reduced formula does not have
to be in CNF. If the reduced formula
has no more than two variables, it
can be converted into a CNF set of
2-clauses.

We can AND the sets of 2-clauses
from all the reduced formulas into
a single 2SAT instance.

If this 2SAT instance is unsatisfiable,
the entire instance is unsatisfiable.
Otherwise, we can take any satisfying
assignment of the 2SAT instance and use
the method desscibed above to find a
satisfying assignment of the entire 3SAT
instance.

Similar arguments show combinations
of type 1, type 2, and type 3 clauses
can be solved in a polynomial number
of steps if the reduced formula of
every index clause family has two
or fewer variables.


Russell
- 2 many 2 count
 | 
Pages: 1
Prev: ICNAAM 2010 Mini-Symposium on Computational Bioimaging and Visualization
Next: CFP with Extended Deadline of Mar. 21, 2010: The 2010 International Conference on Foundations of Computer Science (FCS'10), USA, July 2010