3SAT - Minimum Number of Unit Clauses
RussellE
I show if a 3SAT instance has a satisfiying assignment,
a satisfying assignment can be found in a polynomial
number of steps or all satisfying assignments have at
least three unit clauses.
I can easily create a 2SAT instance from a
3SAT instance by choosing two literals from
each 3clause and making a 2clause. Any
satisfying assignment of the resulting 2SAT
instance will also be a satisfying assignment
of the 3SAT instance.
Assume I am given the following 3SAT instance:
(a+b+c)(~a+b+c)(a+~b+~c)(~a+~b+~c)
Each 3clause has three "edges":
1) Two lowest order literals
2) Lowest and highest order literals
3) Two highest order literals
The 3clause (a+b+c) has three "edges":
1) (a+b)
2) (a+c)
3) (b+c)
I can make three 2SAT instances from the
example above by choosing all edge 1's,
or all edge 2's, or all edge 3's:
1) (a+b)(~a+b)(a+~b)(~a+~b)
2) (a+c)(~a+c)(a+~c)(~a+~c)
3) (b+c)(~b+~c)
The first 2SAT instance is unsolvable.
This tells us any satisfying assignment
of the 3SAT instance must have at least
one unit clause where the highest order
literal is True and the other literals
are False. Since the first 2SAT instance
is unsolvable, we can add the following
clause to the 3SAT instance:
(~a~bc + a~bc + ~ab~c + ab~c)
Similarly, since the second 3SAT instance
is unsolvable, we know any satisfying
assignment of the 3SAT instance must have
at least one unit clause where the middle
order literal is True and the other two
literals are False. We can now add another
clause to our 3SAT instance:
(~ab~c + ab~c + ~a~bc + a~bc)
Notice, this is the same clause we got before.
In fact, this is a list of the only satisfying
assignments for the 3SAT instance. Normally,
we will not be so lucky.
The 3SAT instance can be reduced to the third
2SAT instance using resolution. Consider
the first satisfying assignment:
~a~bc
(a+b+C)(~A+b+C)(a+~B+~c)(~A+~B+~c)
As expected, there is at least one unit clause
where the highest order literal is True: (a+b+C),
and one unit clause where the middle literal
is True: (a+~B+~c).
The other satisfying assignments will all have
at least two unit clauses:
a~bc
(A+b+C)(~a+b+C)(A+~B+~c)(~a+~B+~c)
~ab~c
(a+B+c)(~A+b+C)(a+~b+~C)(~A+~b+~C)
ab~c
(A+B+c)(~a+B+c)(A+~b+~C)(~a+~b+~C)
By solving three 2SAT instances we will either
find a satisfying assignment or prove all
satisfying assignments have at least three
unit clauses.
Has anyone seen anything similar to this?
I think it may be possible to show every
satisfying assignment must have a minimum
number of clauses where the clause is
satisfied twice, like (~A+~B+~c). I would
also like to find a way to increase the
minimum number of unit clauses a satisfying
assignment must have, maybe by creating
other 2SAT instances.
I think this is also related to forced 2clauses.
In this example, I can show the two 2clauses
(b+c)(~b+~c) are forced.
Russell
- 2 many 2 count