OKlibrary  0.2.1.6
Var< Matrix, Formula > Class Template Reference

Translating an adjacency matrix M and a desired max biclique-number max_bc into the (boolean CNF) SAT problem F. More...

#include <TransformationsBiclique.hpp>


Detailed Description

template<class Matrix, class Formula>
class Var< Matrix, Formula >

Translating an adjacency matrix M and a desired max biclique-number 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.


The documentation for this class was generated from the following file: