Plans regarding biclique partitions of (general) graphs.
More...
Go to the source code of this file.
Detailed Description
Plans regarding biclique partitions of (general) graphs.
 Todo:
 Translations to clausesets

See "Conflict graph" in ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/plans/general.hpp

Organisation:

Does this belong to ComputerAlgebra/Graphs, or to ComputerAlgebra/Satisfiability?

Formation of conflict graphs etc. seem naturally to belong to Satisfiability/ConflictCombinatorics, since these graphs are first of all tools to analyse clausesets.

What about translations of biclique partitions (and of graphs for given methods of biclique partitions) into clausesets?

Placing them in Satisfiability/ConflictCombinatorics seems again most natural; perhaps in a submodule "Realisations" ?
 Todo:
 The conjecture of [Galesi, Kullmann]

Using the (deprecated) Mupadfunctions, the conjecture is that if ist_exakt_transversal(M) is true, then ist_speziell_exakt_transversal(M) is true.

This should be equivalent to the statement, that every minimally unsatisfiable clauseset F, whose conflict multigraph is a complete bipartite graph, has a readonce resolution refutation.

First approach for searching for a counterexample:

Enumerate or sample biclique partitions of complete bipartite graphs.

Get the corresponding clauseset.

Perform subsumptionelimination.

Remove satisfiable clausesets (via SAT or via the decision procedure for exact transversal hypergraphs).

Check the clauseset for the special condition.

We need to implement a test for the special condition:

This should be a simple recursive procedure.

ist_speziell_exakt_transversal(M) is a starting point (but it doesn't recursively check the condition).
 Todo:
 NPcompleteness of determining bcp

Find literature on the NPcompleteness of the determination of the biclique partition number bcp(G).

Implement it.
Definition in file general.hpp.