npycomp.reductions.

threesat_to_clique

npycomp.reductions.threesat_to_clique(clauses: list[tuple[str]]) → tuple[list[list[int]], int]

Convert a 3SAT problem to a clique problem.

Consider a 3-SAT formula with \(n\) clauses \(\phi = C_1 \land C_2 \land C_n\), where \(C_i\) is a clause consisting of the disjunction of at most three literals: \(C_i = (l_1^i \lor l_2^i \lor l_3^i)\). The reduction to a clique problem is as follows.

Construct a graph \(G(V, E)\) with a vertex for each literal \(l_i^j\) in each clause \(j\). For every pair of vertices, and an edge between them if they are (i) not part of the same clause, and (ii) are not in contradiction, i.e., they either refer to different variables, or refer to the same variable but are not complements of each other.

The resulting graph \(G\) has a clique of size \(n\) if and only if the 3-SAT formula \(\phi\) is satisfiable, where \(n\) is the number of clauses in the formula.

Parameters:

clauseslist

A list of clauses in conjunctive normal form. Each clause is a tuple of at most three literals.

Returns:

tuple

The adjacency matrix of the graph and the number of clauses.