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.

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" ?
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).
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.