3SAT - Forced Unit Clauses
RussellE
I show one reason why every satisfying assignment of some
3SAT instances must a minimum number of unit clauses.
I can create three "edge" clauses from any 3clause.
For example, the three edges for (a+b+c):
1) (a+b)
2) (a+c)
3) (b+c)
Assume I replace each 3clause in a 3SAT
instance with the corresponding edge clauses.
Any satisfying assignment of this "edge" 2SAT
instance is also a satisfying assignment for
the original 3SAT instance. If this "edge" 2SAT
instance is satisfiable, then the original 3SAT
instance is "renamable Horn". There
exist a satisfying assignment with no
unit clauses.
If the "edge" 2SAT instance is unsatisfiable,
then at least one edge is unsatisfied in
every satisfying assignment. At most, m edge
clauses can be unsatisfied, where m is the
number of 3clauses in the original 3SAT instance.
No more than one edge per 3clause can be
unsatisfied in any satisfying assignment.
Consider the following 3SAT instance:
(a+b+c)(~a+b+c)(a+~b+c)(~a+~b+c)
We have the following four (of 12) edge clauses:
(a+b)
(~a+b)
(a+~b)
(~a+~b)
One of these edges must be unsatisfied
for any assignment of the variables A and B.
This proves the 3SAT instance is not renamable
Horn and at least one edge clause will be
unsatisfied in every satisfying assignment.
This shows every satisfying assignment will
have at least one unit clause.
Since one of the edge clauses must be satisfied
twice, this also shows every satisfying assignment
must have at least one clause that is not a unit clause.
Russell
- 2 many 2 count