OKlibrary  0.2.1.6
general.hpp File Reference

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 clause-sets
• See "Conflict graph" in ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/plans/general.hpp
• Organisation:
1. Does this belong to ComputerAlgebra/Graphs, or to ComputerAlgebra/Satisfiability?
2. Formation of conflict graphs etc. seem naturally to belong to Satisfiability/ConflictCombinatorics, since these graphs are first of all tools to analyse clause-sets.
3. What about translations of biclique partitions (and of graphs for given methods of biclique partitions) into clause-sets?
• Placing them in Satisfiability/ConflictCombinatorics seems again most natural; perhaps in a sub-module "Realisations" ?
Todo:
The conjecture of [Galesi, Kullmann]
• Using the (deprecated) Mupad-functions, 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 clause-set F, whose conflict multigraph is a complete bipartite graph, has a read-once resolution refutation.
• First approach for searching for a counter-example:
1. Enumerate or sample biclique partitions of complete bipartite graphs.
2. Get the corresponding clause-set.
3. Perform subsumption-elimination.
4. Remove satisfiable clause-sets (via SAT or via the decision procedure for exact transversal hypergraphs).
5. Check the clause-set for the special condition.
• We need to implement a test for the special condition:
1. This should be a simple recursive procedure.
2. ist_speziell_exakt_transversal(M) is a starting point (but it doesn't recursively check the condition).
Todo:
NP-completeness of determining bcp
• Find literature on the NP-completeness of the determination of the biclique partition number bcp(G).
• Implement it.

Definition in file general.hpp.