OKlibrary  0.2.1.6
general.hpp File Reference

Plans for Maxima-components related to conflict-patterns of clause-sets. More...

Go to the source code of this file.

Detailed Description

Plans for Maxima-components related to conflict-patterns of clause-sets.

Todo:
Create milestones
Todo:
Write tests
Todo:
Write docus
Todo:
Conflict graph
• Write gcg_lcs(FF), the general conflict graph of a labelled clause-set.
1. Edge-labels are [[C,D],v], where C,D are clause-labels and v a variable, such that the clauses clash in literal v.
• Since gcg is a functor, also write gcg_homfcs(f), the mapping for homomorphisms f.
1. Since f doesn't know its domain and codomain, perhaps they need to be supplied additionally.
• Analogously, write gcdg_lcl(FF), the general conflict digraph of a labelled clause-set, and gcdg_homfcs(f).
• An important topic is how to "realise" (directed/undirected) conflict graphs; perhaps for special methods we have "Realisations.mac" ?
1. "Realising" here means to find a clause-set with the given graph as conflict graph.
2. In general this is done by finding a biclique partition (in the boolean case) of the (general) graph, and interpreting the bicliques as variables and the vertices as clauses.
3. Thus here we have a mapping with two arguments, the (general) graph and the bipartitioning; a general question is whether there are reasonable methods which just need the (general) graph (and thus automatically provide the biclique partitioning), and which even yield functors?
4. Most elementary is the trivial biclique partition of a general digraph, which is also functorial; this yields clause-sets (with clashing "clauses" iff loops are present) where every variable has (1,1)-occurrence.
5. More generally we can use maximal out-stars; this yields Horn clause-sets where every variable is singular; can this process be made functorial??
Todo:
Hermitian rank
• DONE It seems we should use hermitian_rank_charpoly instead of hermitian_rank for hermitian_rank_cs.
• Computation of the characteristic polynomial of a clause-set:
1. What is the characteristic polynomial of the empty square matrix?
• Of course, there are many graphs associated with a clause-set, but it seems that only the characteristic polynomial of the conflict multigraph is of interest?
1. So that we can speak of "the" characteristic polynomial?
2. Or should we speak of the "characteristic conflict-polynomial"?
• What is the meaning of charpoly_cs(F) ?
1. Of course, the roots of charpoly_cs(F) have some meaning.
2. But what about the numeric values of the coefficients?
Todo:
Relations to other modules
Todo:
mcind_cs, cind_cs:
• DONE The naming should reflect the special method used (here using transversals).
• Likely the best is just to refer to all possible ways of computing maximal independent sets of a hypergraph (or, of a graph; likely one can take advantage of this more special situation).
• It seems not to be worth to develop an algorithm which computes directly all independent sets?

Definition in file general.hpp.