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 = (x_{1} ∨ x_{2}) ∧ (~x_{1} ∨ ~x_{2}) ∧ (~x_{1} ∨ x_{2})

This formula has just one mixed clause (the third one) and is satisfiable if x_{1} is false and x_{2} is true. The formula becomes unsatisfiable if we add the clause (x_{1} ∨ ~x_{2}), 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 x_{1} through x_{m}. The first instance of x in F will be replaced by x_{1}, the second by ~x_{2}, the third by x_{3}, and so on down. We then need to basically add the rules x_{1} ≡~x_{2} ≡ x_{3} … (forcing each new literal we replaced x with to all have the same truth values). in CNF form, that’s equivalent to the clauses: (x_{1} ∨ x_{2}) ∧ (~x_{2} ∨ ~x_{3}) ∧ (x_{3} ∨ x_{4}) .. 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 x_{i} 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.