Tag Archives: LO3

Generalized Satisfiability

We’re starting a new section and a lot of the introductory problems have been covered elsewhere.

LO1 is Satisfiability

LO2 is 3-Satisfiability

LO3 is Not all Equal 3SAT

LO4 is One-In-Three 3SAT

LO5 is Maximum 2SAT

After that we finally get to a new problem:

The Problem: Generalized Satisfiability.  This is problem LO6 in the appendix.

The description: Given a list of positive integers k1 through km and a sequence S = <R1..Rm>, where each Ri is a set of strings of ki “T” or “F” symbols.  We’re also given a set U of variables, and a set of collections C1 through Cm.  Each Ci contains a ki-tuple of variables from U.

Can we assign a truth value (“T” or “F”) to each variable in  U such that for each tuple in Ci the truth value of each variable in the tuple matches the sequence of true and false values in Ri?

Example: Let all ki = 3, and m = 2.  R1 = {(T,T,T), (F,F,F)}  R2 = {(T,F,F). (F,T,T)}

U = {x1, x2, x3}.  C1 = (x1, x2, x3}.  C2 = {x1, x2, x3}

So, the question is: Can we assign truth values to x1 x2 and x3 so that the truth values map to a sequence in both R0 and R1?  Since we have the same sequences of the same variables in both sets, the answer is no.

But, suppose we change C2 to (x4, x2, x3).  Then we can set x1, x2, and x3 to true and x4 to false.  This will let the sequence in C1 map to the (T,T,T) sequence in R1, and the sequence in C2 map to the (F,T,T) sequence in R2.

Reduction: This reduction is in Shaefer’s paper, and it reduces from 3SAT.  The idea is that we will build 4 R sets, thinking of them as functions.  So:

R0 = {R(x,y,z) | x or y or z is true} = {(T,T,T), (T,T,F), (T,F,T), (T,F,F), (F,T,T), (F,T,F), (F,F,T)}

R1 =Same idea, but  “~x or y or z is true”

R2 = “~x or ~y or z is true”

R3 = ” ~x or ~y or ~z is true”

Once we’re given a CNF instance, we replace each clause in the formula with one of the Ri formulas.  Then build a C set that uses the variables in the clause.  So, for example, if a clause in the CNF formula was ~x2 ∨ x5 ∨ ~x7, we’d make the element in R corresponding to the clause R2, and we’d use the C formula (x2, x7, x5).  Notice that we changed the order of the variables in the C set because R2 expects its negated literals first.

Notice that we can find a way to assign the variables truth values to make each Ci map to its R set, we have satisfied the clause.  So this new construction is satisfiable if and only if the 3SATinstance was satisfiable.

Difficulty: Making the construction is probably a 5, mostly because you need a good way to explain how you’re making the R sets.  The hardest thing here though is understanding what the problem says.

Not All Equal 3SAT

This is jumping ahead a little, but this is a variant of 3SAT that will be helpful in the future (actually, for the next problem)

The problem: Not-All-Equal-3SAT (NAE3SAT).  This is problem LO3 in the appendix.

The description: Just like 3SAT, except instead of requiring at least one of the literals in each clause to be true, we’re requiring at least one literal to be true and at least one literal to be false.  So we’re removing the case where all three literals can be true.

Notice that if we have an assignment of variables that is a NAE3SAT solution, then if we negate all of the variables, we still have a NAE3SAT solution

The reduction: From regular 3SAT.  We’re given a formula that is a collection of 3-literal clauses.  For each clause (x1 ∨ x2 ∨ x3) we create a new variable ci (for clause i) and add 2 clauses to our NAE3SAT instance:

(x1∨ x2 ∨ ci) and (x3 ∨ ~ci ∨ F)  (Where “F” is the constant value false.  We’ll talk more about this later)

The idea is that ci is there to “fix” the clause.  If the original clause was satisfiable because of x1 or x2, then ci can be false, and its negation can make the second clause true.  If the original clause was satisfiable because of x3, we can make ci true.  If the original clause had all three literals satisfiable, we can make ci false, and become an acceptable NAE3SAT solution.

Note that because the definition of NAE3SAT (and, for that matter, regular 3SAT) is defined in terms of collections of 3 variables, the constant value false we used above isn’t strictly legal.  We’ve really just shown “NAE3SAT with some constants replacing variables” is NP-Hard.  To show “normal” NAE3SAT is NP-Hard, we need to reduce the fixed constant version into the normal version:

Given an instance of NAE3SAT with fixed constants, we create 2 new variables xT and xF.  We replace all instances of the constant value true with xT, and all instances of the constant value false with xF.  We also add one additional clause:

(xT ∨ xT ∨ xF).

Note that this new clause is only NAESatisfiable if xT != xF.  We can’t directly bind xT to true and xF to false because if you take a NAE3SAT solution and negate all literals, you get another NAE3SAT solution.  But because of that, this is NAESatisfiable if and only if the original formula is.

Difficulty: It depends on what you give them.  If you make them do everything I did above, I’d say it’s an 8.  If you let them stop at the NAE3SAT with fixed constants, then maybe a 7.