OKlibrary
0.2.1.6

Translating an adjacency matrix M and a desired max bicliquenumber max_bc into the (boolean CNF) SAT problem F. More...
#include <TransformationsBiclique.hpp>
Translating an adjacency matrix M and a desired max bicliquenumber max_bc into the (boolean CNF) SAT problem F.
Given the matrix M of dimension dim, and two nodes (i.e., indices) i and j, we have M(i,j) conflicts between i and j. Using indices 0 <= v < M(i,j), for each such conflict we have 2 * max_bc variables, such that exactly one of them must become true, where the first chunk of max_bc variables asserts that this conflict is in the corresponding biclique with orientation from "left to right", while the second chunk of max_bc variables refers to the opposite orientation.
Definition at line 155 of file TransformationsBiclique.hpp.