OKlibrary  0.2.1.6
Conflicts.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.1.2008 (Swansea) */
00002 /* Copyright 2008 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/CombinatorialMatrices/Lisp/Basics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/LinearAlgebra/Lisp/QuadraticForms.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Graphs/Lisp/Basic.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Basics.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/IndependentSets.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Graphs/Lisp/IndependentSets.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Graphs/Lisp/Colouring.mac")$
00030 
00031 
00032 /* *****************
00033    * Constructions *
00034    *****************
00035 */
00036 
00037 /* The conflict-matrix (as a square combinatorial matrix) of a clause-set */
00038 cm_cs(F) := [F, lambda([C,D], length(intersection(C,comp_sl(D))))]$
00039 /* cm_cs(F) = 1/2 (cl_varint_scom_cs(F) - cl_int_scom_cs(F)). */
00040 
00041 /* The conflict-graph of a clause-set */
00042 cg_cs(F) := [F, subset(powerset(F,2),lambda([S], 
00043   block([L:listify(S)], return(clashp(L[1],L[2])))))]$
00044 /* cg_cs(F) = com2g(cm_cs(F)) */
00045 cg_fcs(F) := cg_cs(fcs2cs(F))$
00046 
00047 /* The hypergraph of maximal conflict-independent subsets of a 
00048    clause-set; i.e., all maximal conflict-free subsets. */
00049 mcind_cs(F, Ind) := Ind(cg_cs(F))$
00050 mcind_cs_trrs(F) := mcind_cs(F, independence_hyp_trrs)$
00051 /* The hypergraph of all conflict-independent subsets of a clause-set */
00052 cind_cs_trrs(F) := subset_closure_hyp(mcind_cs_trrs(F))$
00053 
00054 
00055 /* ************
00056    * Measures *
00057    ************
00058 */
00059 
00060 /* The number of conflicts of a boolean clause-set F. */
00061 nconflicts(F) := sum_scom(cm_cs(F))/2$
00062 /* The "reduced number of conflicts" of a boolean clause-set F 
00063    (counting only one possible conflict per pair of clauses). */
00064 rnconflicts(F) := length(cg_cs(F)[2])$
00065 
00066 
00067 /* Using function h for computing the hermitian rank of a matrix. */
00068 hermitian_rank_cs_h(F,_h) := _h(scom2m(cm_cs(F)))$
00069 /* The hermitian rank of a boolean clause-set F. */
00070 hermitian_rank_cs(F) := hermitian_rank_cs_h(F,hermitian_rank_charpoly)$
00071 
00072 /* The hermitian defect of a boolean clause-set F. */
00073 hermitian_defect_cs(F) := ncl_cs(F) - hermitian_rank_cs(F)$
00074 
00075 /* The characteristic polynomial of a clause-set, in variable x. */
00076 charpoly_cs(F) := if emptyp(F) then 0 else 
00077  block([M : scom2m(cm_cs(F)), ratmx : true],
00078   return(charpoly_m(M)))$
00079 /* The eigenvalues of a clause-set, in analytical form. */
00080 eigenvalues_cs(F) := if emptyp(F) then [] else
00081  eigenvalues(scom2m(cm_cs(F)))$
00082 /* The eigenvalues of a clause-set, numerically. */
00083 eigenvaluesnum_cs(F) := if emptyp(F) then [] else
00084  eigens_by_jacobi(scom2m(cm_cs(F)),bigfloatfield)[1]$
00085 
00086 
00087 /* The conflict-independence number of a clause-set F, using function ind_num_f
00088    for computing the independence number of a graph */
00089 independence_number_cs(F, ind_num_f) :=ind_num_f(cg_cs(F))$
00090 /* Using the Maxima-function */
00091 independence_number_m_cs(F) := independence_number_cs(F, independence_number_gr_m)$
00092 
00093 /* The conflict-partition number of a clause-set F, using function part_num_f
00094    for computing the partition number of a graph */
00095 /* The conflict-partition number of F is <= 1 iff F is hitting. */
00096 partition_number_cs(F, part_num_f) := part_num_f(cg_cs(F))$
00097 /* Using the Maxima-function */
00098 partition_number_m_cs(F) := partition_number_cs(F, partition_number_gr_m)$
00099 
00100 
00101 /* *********
00102    * Tests *
00103    *********
00104 */
00105 
00106 /* Whether a clause-set is graphic (the conflict multigraph
00107    is a graph) */
00108 graphiccsp(F) := is(max_com(scom2com(cm_cs(F))) <= 1)$
00109 
00110 /* Whether a clause-set is bipartite (the conflict-graph is bipartite):
00111 */
00112 bipartite_cs_p(F) := bipartite_g_p(cg_cs(F))$
00113 bipartite_fcs_p(FF) := bipartite_g_p(cg_fcs(FF))$
00114 
00115 /* The Alon-Saks-conjecture for graphs states that the chromatic number
00116    is at most the biclique-partion number + 1.
00117    We transfer this to clause-sets, and return unknown in case the clause-set
00118    is not graphic, while otherwise a list is returned with first entry a
00119    boolean on whether the conjecture is true for this case or not.
00120    The second entry is again a boolean, about the (likely false) strengthened
00121    conjecture where n(F)+1 is lower-bounded by h(F)+1.
00122    The remaining three entries are the numbers involved. */
00123 alon_saks_cs(F) := if not graphiccsp(F) then unknown else
00124  block([chi : chromatic_number_gr_m(cg_cs(F)), 
00125         r : hermitian_rank_cs(F), 
00126         n : nvar_cs(F)],
00127   return([is(chi <= n+1),is(chi <= r+1),chi,r+1,n+1]))$
00128