Tag Archives: Satisfiability

Non-Circular Satisfiability

The next reduction uses a new variant of Satisfiability, so I figured it would be worth making a separate post for it.

The problem: Non-Circular Satisfiability.  This problem is not in the appendix.

The description: A CNF-Satisfiability clause is mixed if it contains both variables and their negations.  A Satisfiability formula is non-circular if each variable occurs in a mixed clause at most once.  Given a non-circular satisfiability formula, is it satisfiable?

Example: This is actually a more general version of Monotone Satisfiability– in Monotone Sat, no mixed clauses can exist.  So all Monotone formulas are also Non-Circular.

Notice that we’re not necessarily restricting things to 3Sat clauses- we can have more or less than 3 variables per clause.  So here is a (satisfiable) instance:

F = (x1 ∨ x2) ∧ (~x1 ∨ ~x2) ∧ (~x1 ∨ x2)

This formula has just one mixed clause (the third one) and is satisfiable if x1 is false and x2 is true.  The formula becomes unsatisfiable if we add the clause (x1 ∨ ~x2), but then we would have both variables be in a second mixed clause.

Reduction: The easy way is to just do this by restriction from Montone Sat.  (Given a monotone sat formula, it’s automatically non-circular, so we’re done).  But if we want an actual reduction, we can use the paper by Papadimitriou, Bernstein, and Rothnie which has the next two reductions in G&J and uses this problem for the first one.  They also show the reduction for this problem in their paper and reduce from regular CNF-SAT.  So we have a formula F.  For each variable x in F, suppose x appears m times in F. Create m new variables x1 through xm.  The first instance of x in F will be replaced by x1, the second by ~x2, the third by x3, and so on down.  We then need to basically add the rules x1 ≡~x2 ≡ x3 …  (forcing each new literal we replaced x with to all have the same truth values).  in CNF form, that’s equivalent to the clauses: (x1 ∨ x2) ∧ (~x2 ∨ ~x3) ∧ (x3 ∨ x4) .. and so on down.  This means our new formula is equivalent to F (and is satisfiable when F is).  Each of these new clauses is non-mixed.  The only other occurrence of each xi variable is the one time it replaces x in the original F, which may or may not be a mixed clause, but either way, that means each variable appears in at most one mixed clause.

Difficulty: 3.  This is about as hard as the Monotone Sat reduction.

Protected: Planar 3-Satisfiability

This content is password protected. To view it please enter your password below: