Transformations.hpp File Reference

Plans regarding transforming the problem of finding biclique partitions into other problems. More...

Go to the source code of this file.

Detailed Description

Plans regarding transforming the problem of finding biclique partitions into other problems.

Parameters for encoding
  • The most basic parameter is an upper bound on the number of biclique, that is, an upper bound on the number of variables.
  • More specifically, we could have a list of biclique sizes, that is, for every variable we specify the number of occurrences.
  • When can also specify the number of literal occurrences, by fixing the sizes of the sides of the bicliques.
  • The size of a clause corresponding to a vertex is between 1 and the degree of the vertex (we should consider here only connected graphs), namely it is exactly the number of bicliques the vertex participates.

    Edge-centered SAT encoding
    Vertex-centred SAT encoding
    • A biclique-partition of a multigraph G, using at most k parts, can be naturally encoded into a mapping from V to {-k, ..., k} - {0}, assigning to each vertex its biclique-number together with the "side".
    • However, if the degree of a vertex v is d(v), then we must have 1 <= l_i <= d(v) "copies" of v (since v will participate in exactly d(v) bicliques).
      1. l_i is the length of the clause corresponding to this vertex.
      2. So the strength of this model is that the clause-lengths can naturally be prescribed.
      3. Of course, this is also a weakness; apparently unavoidable.
    • No two copies of a vertex can be contain in the same biclique.
    • In general we need to ensure that all edges have been covered (while the partitioning condition is automatically given now):
      1. Natural is to use for each vertex v a cardinality constraint requiring that together for all the copies we have exactly d(v) edges.
      2. One could also specify that the total number of edges is as required.
      3. On the other end, one could specify for each copy of v the number of neighbours.
      4. So literal regularity of the corresponding clause-set is easy to require.
    • For each 1 <= i <= k the vertices with numbers -i,+i must possibly form a complete bipartite graph, that is, from every vertex with -i to every vertex with +i there is an edge.
    • That we have a biclique-partition is then automatically achieved, since each of the copies participate in a biclique!
    • This looks quite nice.
      1. A natural application is when searching for a uniform clause-set.
      2. Variable degrees for variable 1 <= i <= k can be naturalled specified by cardinality constraints on the number of copies of vertices which get values -i or +i.
      3. And also literal degrees can be easily prescribed (by cardinality constraints), again just counting copies of vertices; see also above for the issue of ensuring that enough edges are there.
      4. It would be nice if one could apply it to search for ABDs, however therefore we must also know the conflict matrix; see ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/plans/AssociativeBlockDesigns.hpp
    • Find reductions of the problem of finding biclique partitions to other problems (than SAT).
    • Perhaps there are more closely related problems, where the translation is more direct.

Definition in file Transformations.hpp.