(3,3)-SAT

Task number: 4002

Consider a logical formula of the form \( (x_1 \lor \lnot x_2 \lor \ldots) \land (x_3 \lor \ldots) \land \ldots \), i.e. one that is a conjunction of clauses, which are disjunctions of literals and each literal is either a variable or its negation. A formula is satisfiable if it is possible to substitute true/false for the variables so that the whole formula is true.

Prove that any formula whose each clause contains exactly 3 literals and each variable occurs in just 3 different clauses is satisfiable.

  • Hint

    Convert to the problem of finding a matching in a bipartite graph.

  • Solution

    Create a bipartite graph of incidence, where on one side there are clauses and on the other variables that occur in them, either as a positive or as a negative literal.

    This graph is 3-regular bipartite, so it contains a perfect pairing.

    Perfect matching determines for each clause which variable guarantees its satisfiability. We set the value of the variable to true if it occurs in the clause as a positive literal; and false otherwise.

    Note: if a variable occurred more than once in the same clause, it would not affect the fulfillment in any way. In the incidence graph, such cases would cause multiple edges. Triple edges form components, they are easy to treat. If \( (u, v) \) is a double edge, \( u \) and \( v \) can be removed from the graph and joined by the edge of their remaining neighbors. This operation does not affect the existence of perfect pairing (or edge 3-colorings).

    Note that \( (k, k) \)-SAT is always satisfiable if the variables have occurrences in different clauses. However, the described multiple edge reduction only works for \( (3{,}3) \)-SAT.

Difficulty level: Moderate task
Proving or derivation task
Cs translation
Send comment on task by email