OKlibrary  0.2.1.6
HittingClauseSets.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 12.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 2012, 2013 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/Backtracking/SplittingTrees.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Deficiency2.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Graphs/Lisp/Basic.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Counting/InclusionExclusion.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/DP-Reductions.mac")$
00032 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/MinVarDegrees.mac")$
00033 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Basics.mac")$
00034 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac")$
00035 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00036 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")$
00037 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00038 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/Auxiliary.mac")$
00039 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/InverseSingularDP.mac")$
00040 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/TseitinTranslation.mac")$
00041 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Strings.mac")$
00042 /* Below there are further includes (delayed). */
00043 
00044 
00045 /* ***************************************
00046    * Representations via splitting trees *
00047    ***************************************
00048 */
00049 
00050 /* Given a splitting tree (a tree whose inner nodes are labelled by boolean
00051    literals), extract the hitting clause-set given by the false-leaves
00052    (which is unsatisfiable iff the tree is complete; the "clause-set"
00053    contains a tautological clause (this for the CNF interpretation) iff a
00054    variable occurs twice on some  path). */
00055 /* The unsatisfiable hitting clause-sets generated in this way are the
00056    "tree hitting clause-sets", and with tautological clauses removed these
00057    are exactly those hitting clause-sets which have a read-once resolution
00058    refutation.
00059    The other hitting clause-sets created are subsets of tree hitting
00060    clause-sets. */
00061 treehittingcls_st(T) := setify(usat_clauses_st(T))$
00062 /* The dual hitting clause-set, representing the unterlying CNF as DNF */
00063 dualtreehittingcls_st(T) := setify(sat_pass_st(T))$
00064 /* The full representation, consisting of a hitting clause-set representing
00065    the falsifying assignments (as CNF), and of a hitting clause-set
00066    representing the satisfying assignments (as DNF, i.e. as sets of
00067    partial assignments). */
00068 hitting_cls_rep_st(T) := [treehittingcls_st(T), dualtreehittingcls_st(T)]$
00069 
00070 /* Convenience functions, which generate splitting trees by backtracking
00071    solvers (without backtracking); the heuristics needs to be
00072    supplied): */
00073 treehittingcls_fcs(FF,h) := treehittingcls_st(dll_simplest_st(FF,h))$
00074 dualtreehittingcls_fcs(FF,h) := dualtreehittingcls_st(dll_simplest_st(FF,h))$
00075 hitting_cls_rep_fcs(FF,h) := hitting_cls_rep_st(dll_simplest_st(FF,h))$
00076 /* The variations where the splitting trees first are condensed (this
00077    is sensible for analysing boolean functions): */
00078 treehittingcls_condensed_fcs(FF,h) := treehittingcls_st(condense_st(dll_simplest_st(FF,h)))$
00079 dualtreehittingcls_condensed_fcs(FF,h) := dualtreehittingcls_st(condense_st(dll_simplest_st(FF,h)))$
00080 hitting_cls_rep_condensed_fcs(FF,h) := hitting_cls_rep_st(condense_st(dll_simplest_st(FF,h)))$
00081 
00082 
00083 /* **************
00084    * Generators *
00085    **************
00086 */
00087 
00088 /* An unsatisfiable uniform clause-set F with clause-length k has at least
00089    2^k clauses, and the minimum is attained exactly for the uniform hitting
00090    clause-sets with clause-length k and 2^k clauses.
00091 
00092    The two extreme cases are given by full_fcs(n) (with maximal deficiency)
00093    and by the following special SMUSAT(1) clause-sets (with minimal
00094    deficiency), which are (up to renaming) exactly the uniform elements of
00095    SMUSAT(1) with clause-length k.
00096 */
00097 uniform_usat_hitting_min(k) := treehittingcls_st(complete_st_alldifferent(k))$
00098 uniform_usat_hitting_max(k) := full_cs(k)$
00099 
00100 /* The up to isomorphism unique unsatisfiable hitting clause-set
00101    with n variables and of deficiency 2^n - n - 1;
00102    non-singular iff n >= 3. */
00103 /* Prerequisite: n >= 1. */
00104 nearly_full_hitting_fcs(n) := block([FF : full_fcs(n)],
00105   return([FF[1], adjoin(setn(n-1), setdifference(FF[2], {setn(n), adjoin(-n,setn(n-1))}))]))$
00106 
00107 /* An unsatisfiable non-singular hitting clause-set with m+1 variables and
00108    deficiency 2^m - m + 1, while the minimum var-degree is 2^m.
00109    Prerequisite: m >= 2.
00110 */
00111 over_full_hitting_fcs(m) := block(
00112  [n : m+1, A : full_cl(2), B],
00113   B : full_cs_v(setmn(3,n)),
00114   [setn(n), union({A[1],A[2]}, or_cs2({A[3]}, B), or_cs2({A[4]}, B))])$
00115 /* Remarks: over_full_hitting_fcs(m) realises the maximum min-var-degree for
00116    clause-sets of deficiency 2^m-m+1.
00117 */
00118 
00119 
00120 /* Saturated minimally unsatisfiable Horn clause-sets with k variables: */
00121 smusat_horn_cs(k) := treehittingcls_st(horn_st(k))$
00122 /* Standardised (trv[] -> 1, trv[2] -> 2, trv[2,2] -> 3 etc.): */
00123 smusat_horn_stdfcl(k) := [create_list(i,i,1,k),
00124  endcons(setmn(-k,-1),create_list(setify(cons(i,create_list(-j,j,1,i-1))),i,1,k))]$
00125 smusat_horn_stdfcs(k) := fcl2fcs(smusat_horn_stdfcl(k))$
00126 /* Statistics: */
00127 nvar_smusat_horn(k) := k$
00128 ncl_smusat_horn(k) := k+1$
00129 ncl_list_smusat_horn(k) := if k=0 then [[0,1]] else
00130  endcons([k,2], create_list([i,1],i,1,k-1))$
00131  nlitocc_smusat_horn(k) := k*(k+1)/2 + k$
00132 
00133 /* More generally, saturated minimally unsatisfiable level-l Horn clause-sets
00134    with k variables: */
00135 smusat_genhorn_cs(k,l) := treehittingcls_st(genhorn_st(k,l))$
00136 /* Remark: These tree-hitting clause-sets are saturated MU's of deficiency 1
00137    and of hardness min(k,l).
00138 */
00139 /* The satisfiable variations, adding one new variable to each clause: */
00140 sat_genhorn_cs(k,l) := dualtreehittingcls_st(genhornsat_st(k,l))$
00141 /* Remark: These clause-sets F(k,l) have the following properties:
00142     - let c := c(F(k,l)) be the number of clauses (note that c is also the
00143       number of clauses of smusat_genhorn_cs(k,l))
00144     - deficiency 1-c
00145     - 1-regular hitting clause-sets
00146     - satisfiable
00147     - exactly 2^c-1 many prime implicates (as shown in [Sloan, Soereny, Turan,
00148       On k-term DNF with the largest number of prime implicants, 2007]; also
00149       shown there is that extremality w.r.t. the number of prime implicates
00150       is actually characteristic for the clause-sets obtained from SMU(1) by
00151       adding disjoint non-empty variable-sets to all the clauses)
00152     - exactly hardness min(k,l).
00153 */
00154 /* The negation: */
00155 neg_sat_genhorn_cs(n,k) :=
00156   map(lambda([C], block([x: last(C)], adjoin(-x,disjoin(x,C)))),
00157       sat_genhorn_cs(n,k))$
00158 /* Remark: This is a special case of the negation of doped unsatisfiable
00159    hitting clause-sets according to [Gwynne, Kullmann, 2013].
00160 */
00161 /* The equivalent DNF clause-set: */
00162 dnf_sat_genhorn_cs(n,k) :=
00163   map(lambda([C], block([x: last(C)], adjoin(x,comp_sl(disjoin(x,C))))),
00164       sat_genhorn_cs(n,k))$
00165 /* Remark: This is again a special case of the negation of doped unsatisfiable
00166    hitting clause-sets according to [Gwynne, Kullmann, 2013].
00167 */
00168 
00169 /* The boolean function of sat_genhorn_cs(k,l) in three different
00170    representations, together with neg_sat_genhorn_cs(k,l), which makes an
00171    unsatisfiable clause-set:
00172 */
00173 ext1_sat_genhorn_cs(n,k) := union(sat_genhorn_cs(n,k), neg_sat_genhorn_cs(n,k))$
00174 ext2_sat_genhorn_cs(n,k) := union(dualts_cs(dnf_sat_genhorn_cs(n,k)), neg_sat_genhorn_cs(n,k))$
00175 ext3_sat_genhorn_cs(n,k) := union(rcantrans_cs2cs(dnf_sat_genhorn_cs(n,k)), neg_sat_genhorn_cs(n,k))$
00176 
00177 /* Output of these three clause-sets, in extended Dimacs format: */
00178 output_ext1_sat_genhorn(n,k) := outputext_fcs(sconcat("ext1_sat_genhorn_cs(",n,",",k,")",newline, "c ", created_by_OKlib()), cs2fcs(ext1_sat_genhorn_cs(n,k)), sconcat("E1_SAT_genhorn_",n,"_",k,".ecnf"))$
00179 output_ext2_sat_genhorn(n,k) := outputext_fcs(sconcat("ext2_sat_genhorn_cs(",n,",",k,")",newline, "c ", created_by_OKlib()), cs2fcs(ext2_sat_genhorn_cs(n,k)), sconcat("E2_SAT_genhorn_",n,"_",k,".ecnf"))$
00180 output_ext3_sat_genhorn(n,k) := outputext_fcs(sconcat("ext3_sat_genhorn_cs(",n,",",k,")",newline, "c ", created_by_OKlib()), cs2fcs(ext3_sat_genhorn_cs(n,k)), sconcat("E3_SAT_genhorn_",n,"_",k,".ecnf"))$
00181 
00182 
00183 
00184 /* Example from [Savicky, Sgall, 2000, DNF tautologies with a limited number
00185    of occurrences of every variable]: */
00186 sasg2000 : [setn(4), {{1,-2,4},{2,-3,4},{-1,3,4},{1,2,3},
00187  {1,-2,-4},{2,-3,-4},{-1,3,-4},{-1,-2,-3}}]$
00188 /* Example from [Brouwer, 1999, An associative block design ABD(8,5)]: */
00189 brouwer1999 : [setn(8), {
00190  {1,2,3,4,5},{-1,2,3,4,5},{1,2,3,4,-5},{-1,2,3,4,-5},
00191  {1,2,3,-4,6},{-1,2,3,-4,6},{1,-4,5,-6,7},{-1,-4,5,-6,7},
00192  {2,-4,-6,-7,8},{3,-4,-6,-7,-8},{1,-4,-5,-6,7},{-1,-4,-5,-6,7},
00193  {1,-3,5,6,8},{-1,-3,5,6,8},{2,-3,4,7,-8},{1,-3,5,-7,-8},{-1,-3,5,-7,-8},
00194  {2,-3,4,-6,8},{2,-3,-5,6,8},{1,-3,-5,-7,-8},{-1,-3,-5,-7,-8},
00195  {-3,-4,6,7,-8},{-2,3,5,6,8},{-2,4,6,7,-8},{-2,3,4,-7,-8},
00196  {1,-2,4,-6,7},{-1,-2,4,-6,7},{-2,5,-6,-7,8},{-2,-5,6,7,8},
00197  {1,-2,-5,-7,8},{-1,-2,-5,-7,8},{-2,3,-4,6,-8}}]$
00198 /* The possibly unique (up to isomorphism) result of applying
00199    2-subsumption resolution: */
00200 rbrouwer1999 : [setn(7), {
00201  {-7,-5,-1,3,6},{-7,-4,-2,1},{-7,-4,1,2,3},{-7,-3,-2,1,4},
00202  {-7,-3,2,5},{-7,-2,-1,5,6},{-7,-1,2,3,5},{-7,1,3,4,6},{-6,-5,-1,2,3},
00203  {-6,-4,1,3,7},{-6,-3,1,5,7},{-6,-2,-1},{-6,-1,2,5,7},{-6,1,3,4},
00204  {-5,-3,-2,-1,6},{-5,-3,-2,1,7},{-5,-3,2},{-5,3,6,7},{5,6,7}}]$
00205 
00206 
00207 /* Those formal hitting clause-sets which according to a conjecture by OK+XSZ
00208    realise the maximal number of variables for given deficiency k >= 2
00209    for unsatisfiable hitting clause-sets without singular variables.
00210 */
00211 max_var_hitting_def(k) := if k=2 then musatd2_fcs(3) else
00212   vardisjoint_full_gluing(max_var_hitting_def(k-1), musatd2_fcs(3))$
00213 nvar_max_var_hitting_def(k) := 3 + (k-2) * 4$
00214 /* Alternatives for h >= 2, which realise for deficiencies 2,3,5,9,17,...
00215    the same number of variables, and having hardness h; not isomorphic to
00216    any max_var_hitting_def(k) for h >= 4, since all max_var_hitting_def(k)
00217    for k >= 3 have hardness = 3:
00218 */
00219 max_var_hittingdef2_cs(h) := if h<=3 then max_var_hitting_def(h)
00220  else block([F:max_var_hittingdef2_cs(h-1)],
00221   vardisjoint_full_gluing(F,F))$
00222 def_max_var_hittingdef2_cs(h) := 2^(h-2)+1$
00223 nvar_max_var_hittingdef2_cs(h) := 2^h-1$
00224 
00225 
00226 /* Given a set S of formal hitting clause-sets, compute the set of all
00227   singular hitting extensions by (exactly) k steps (where k is an integer):
00228 */
00229 all_hitting_extensions_k_fcs(S,k) := if k < 0 then {}
00230  elseif k=0 then S else
00231   all_hitting_extensions_k_fcs(lunion(map(all_pre_hitting_extensions_fcs,S)),k-1)$
00232 /* Now returning a set of non-isomorphic representatives: */
00233 all_reps_hitting_extensions_k_fcs(S,k) :=
00234  if k < 0 then {} else block([S : representatives_fcs(S)],
00235    if k=0 then return(S) else
00236     all_reps_hitting_extensions_k_fcs(lunion(map(all_pre_hitting_extensions_fcs,S)),k-1))$
00237 
00238 
00239 /* *********
00240    * Tests *
00241    *********
00242 */
00243 
00244 /* SAT decision for hitting clause-sets: */
00245 sat_decision_hitting_cs(F) := is(satprob_hitting(F) > 0)$
00246 
00247 /* Tests whether a clause-set is a hitting clause-set: */
00248 hittingcsp(F) := block([l : length(F), L : listify(F), break : false],
00249   for i : 1 thru l-1 unless break do for j : i+1 thru l unless break do
00250     if not clashp(L[i], L[j]) then break : true,
00251   return(not break))$
00252 /* hittingcsp(F) = complete_g_p(cg_cs(F)) */
00253 /* Also: hittingcsp(F) iff independence_number_cs(F) <= 1. */
00254 /* Tests whether a clause-set is a 1-regular hitting clause-set: */
00255 hitting1rcsp(F) := block([l : length(F), L : listify(F), break : false],
00256   for i : 1 thru l-1 unless break do for j : i+1 thru l unless break do
00257     if not length(intersection(L[i],comp_sl(L[j]))) = 1 then break : true,
00258   return(not break))$
00259 
00260 
00261 /* Tests whether a clause-set is a tree hitting clause-set: */
00262 treehittingcsp(F) := block([G : var_hyp(cs_to_fcs(F))],
00263   if emptyp(G[1]) then return(is(F = {{}}))
00264   else block([D : apply(intersection, listify(G[2])), v],
00265     if emptyp(D) then return(false)
00266     else (
00267       v : listify(D)[1],
00268       return(
00269         treehittingcsp(apply_pa({v},F)) and treehittingcsp(apply_pa({-v},F))))))$
00270 
00271 /* Tests whether a clause-set is a uniform unsatisfiable hitting clause-set: */
00272 uuhittingcsp(F) :=
00273  hittingcsp(F) and uniformcsp(F) and not emptyp(F) and is(ncl_cs(F) = 2^(length(listify(F)[1])))$
00274 
00275 /* Returns false if F is not an ABD, and otherwise returns (n,k): */
00276 abd_parameters(F) :=
00277  if not uuhittingcsp(F) or not variableregularcsp(F) then false
00278  else [nvar_cs(F), length(listify(F)[1])]$
00279 
00280 /* Checks whether input F is unsatisfiable hitting and reduced w.r.t.
00281    singular DP-reduction: In the negative case returns the empty list,
00282    and otherwise the unit-list containing the deficiency. */
00283 check_hitting_nsing_def(F) := if hittingcsp(F) and nonsingular_csp(F)
00284    and not sat_decision_hitting_cs(F) then [deficiency_cs(F)]
00285  else [];
00286 
00287 
00288 /* **************************************************************
00289    * Necessary conditions for unsatisfiable hitting clause-sets *
00290    **************************************************************
00291 */
00292 
00293 /* Find all clause-length distributions for a given deficiency def,
00294    number of variables n, and m literal occurrences altogether removed
00295    from the clause-list with (n+def) many full clauses, such that
00296    the remaining clause-list fulfills the unsatisfiability-condition,
00297    assuming that it is a hitting clause-set. */
00298 /* More precisely, the output is a set of set-maps, each mapping the available
00299    clause-lengths to their occurrence numbers. */
00300 /* If the output is empty, then no unsatisfiable hiting clause-set F with
00301    deficiency_cs(F) = def, nvar_cs(F) = n and nlitocc_cs(F) = (n+def)*n - m
00302    is possible. */
00303 /* The idea is that the partitions of m = m_1 + ... + m_r are considered,
00304    each entry m_i relating to a different clause from which exactly m_i
00305    literals are removed. */
00306 /* Prerequisite: def,n,m are non-negative integers, def >= 1. */
00307 all_cld_uhit(def,n,m) := block(
00308  [c : n + def, l, res : []],
00309   if n = 0 then /* actually, should be superfluous ??? */
00310     if def = 1 and m = 0 then return({{[0,1]}}) else return({}),
00311   l : c * n,
00312   if m > l then return({}),
00313   for P in ext_integer_partitions(m) do block([L : length(P), nfc],
00314     nfc : c - L, /* no. of full clauses */
00315     if nfc >= 0 then block(
00316      [s : 2^(-n) * nfc + sum(2^(-(n-P[i])),i,1,L)],
00317       if s = 1 then block([cl_dist : sm2hm({})],
00318         if nfc > 0 then set_hm(cl_dist,n, c - L),
00319         for i in P do
00320           set_hm(cl_dist,n-i,ev_hm_d(cl_dist,n-i,0)+1),
00321         res : endcons(hm2sm(cl_dist),res)
00322       ))),
00323   return(setify(res)))$
00324 /* Filtering-out cases which do not allow the min-var-degree
00325    to be at least mvd. */
00326 /* The proof for the condition is that in the variable-clause matrix
00327    there cannot be a row with strictly more than c - mvd zeros, and
00328    thus we can have at most (c - mvd) * n zeros. */
00329 all_cld_uhit_minvd(def,n,mvd) := apply(union,
00330   create_list(all_cld_uhit(def,n,m),m,0,((def+n)-mvd)*n))$
00331 /* The instance where we search for clause-sets where the general upper
00332    bound on the min-var-degree is attained. */
00333 all_cld_uhit_maxminvd(def,n) := all_cld_uhit_minvd(def,n,nonmersenne_rec[def])$
00334 /* Filtering out cases with unit-clauses. */
00335 all_cld_uhit_maxminvd_nu(def,n) := subset(all_cld_uhit_maxminvd(def,n),
00336  lambda([S],is(listify(S)[1][1] # 1)))$
00337 
00338 
00339 /* ****************************************************
00340    * Representing clause-sets via hitting clause-sets *
00341    ****************************************************
00342 */
00343 
00344 /* Decomposition into a list of hitting clause-sets via the Maxima
00345    function max_clique; simple greedy approach by grabbing the largest
00346    clique. */
00347 /* The length of the returned list is an upper bound on the partition
00348    number of the conflict graph. */
00349 hitting_decomposition_m_cs(F) := block([G : g2mg(cg_cs(F)), G2, R : []],
00350  G2 : copy_graph(G),
00351  while graph_order(G2) > 0 do block([M : max_clique(G2)],
00352    R : endcons(setify(M), R),
00353    for v in M do remove_vertex(v, G2)),
00354  map(lambda([M],map(lambda([v],get_vertex_label(v,G)),M)), R))$
00355 
00356 
00357 /* ********************************************************************
00358    * Finding hitting clause-sets with given deficiency "sporadically" *
00359    ********************************************************************
00360 */
00361 
00362 /* Applying partial assignments */
00363 
00364 /* Find all hitting clause-sets of a given deficiency obtained from
00365    a given hitting clause-set by applying partial assignments: */
00366 all_hittinginstances_def(F,k) :=
00367   subset(map(lambda([phi],apply_pa(phi,F)),all_pass(var_cs(F))),
00368          lambda([F],is(deficiency_cs(F)=k)))$
00369 
00370 /* Applying DP-resolution */
00371 
00372 /* Find all hitting clause-sets of a given deficiency obtained from
00373    a given hitting clause-set by applying DP-resolutions.
00374    The variable given as optional third parameter collects the results;
00375    if already set, then it won't be reset.
00376    The variable given as optional fourth argument reflects the permutation
00377    count; if set, then the computation starts with this permutation
00378    (in the order given by listify(permutations)).
00379 */
00380 all_hitting_DP_reductions_def(F,k,[mon]) := block(
00381  [V : var_cs(F),B,result,_res,permutation_count,_pc],
00382  if length(mon) = 0 then (
00383    _res : 'result, _pc : 'permutation_count)
00384  elseif length(mon) = 1 then (
00385    _res : mon[1], _pc : 'permutation_count)
00386  else (
00387    _res : mon[1], _pc : mon[2]),
00388  if not setp(ev(_res)) then _res :: {},
00389  if not integerp(ev(_pc)) then _pc :: 0 else _pc :: max(ev(_pc)-1,0),
00390 
00391  if deficiency_cs(F) = k then _res :: adjoin(F,ev(_res)),
00392  if emptyp(V) then return(ev(_res))
00393  else block(
00394    [P : rest(permutations(V),ev(_pc))],
00395     for p in P do block([G : F],
00396       _pc :: ev(_pc) + 1,
00397       for v in p do (
00398         G : dp_operator(G,v),
00399         if deficiency_cs(G) = k then _res :: adjoin(G,ev(_res)))),
00400     return(ev(_res))))$
00401 
00402 
00403 /* ********************************************************************
00404    * Finding hitting clause-sets with given deficiency systematically *
00405    ********************************************************************
00406 */
00407 
00408 /* The method is to applying 2-subsumption resolution. */
00409 
00410 /* First the basic search algorithms. */
00411 
00412 /* Given a hitting clause-set F, find all (necessarily hitting) clause-sets
00413    derived from F by (exactly) k 2-subsumption resolution-steps without
00414    removing variables. The result is returned, and also iteratively collected
00415    in the variable which is given as quoted third argument. */
00416 derived_hitting_cs(F,k,results_derived_hitting_cs) := (
00417   results_derived_hitting_cs :: {},
00418   derived_hitting_cs_forb(F,k,{}))$
00419 
00420 /* Additionally now a set of forbidden resolution-pairs is given. */
00421 /* Inherits results_derived_hitting_cs. */
00422 derived_hitting_cs_forb(F,k,forb_pairs) :=
00423  if k < 0 then {}
00424  elseif k = 0 then (
00425    results_derived_hitting_cs :: adjoin(F, ev(results_derived_hitting_cs)), {F})
00426  else
00427  block([FP : setdifference(two_subsumption_resolvable_cs(F),forb_pairs), C,D, x, found : false],
00428    for P in FP unless found do (
00429      [C,D] : listify(P), x : resolution_literal(C,D),
00430      if not elementp(var_l(x), var_cs(setdifference(F,P))) then
00431        forb_pairs : adjoin(P, forb_pairs)
00432      else found : true),
00433    if not found then return({}) else
00434      return(union(
00435        derived_hitting_cs_forb(adjoin(resolvent_l(C,D,x),setdifference(F,{C,D})),k-1,forb_pairs),
00436        derived_hitting_cs_forb(F,k,adjoin({C,D},forb_pairs)))))$
00437 
00438 /* More generally, only allow resolution steps such that for the obtained
00439    clause-set predicate pred is true. */
00440 /* Prerequisite: F is a hitting clause-set, pred(F) = true */
00441 /* The predicate can also use the inherited variables
00442    C,D : parent-clause
00443    x : resolution literal
00444    F : original clause-set.
00445 */
00446 derived_hitting_cs_pred(F,k,results_derived_hitting_cs,pred) := (
00447   results_derived_hitting_cs :: {},
00448   derived_hitting_cs_pred_forb(F,k,{}))$
00449 
00450 /* Again the variation with a given set of forbidden pairs. */
00451 /* Inherits results_derived_hitting_cs and pred. */
00452 derived_hitting_cs_pred_forb(F,k,forb_pairs) :=
00453  if k < 0 then {}
00454  elseif k = 0 then (
00455    results_derived_hitting_cs :: adjoin(F, ev(results_derived_hitting_cs)), {F})
00456  else
00457  block([FP : setdifference(two_subsumption_resolvable_cs(F),forb_pairs), C,D,x,G, found : false],
00458    for P in FP unless found do (
00459      [C,D] : listify(P), x : resolution_literal(C,D),
00460      G : adjoin(resolvent_l(C,D,x),setdifference(F,P)),
00461      if not pred(G) then
00462        forb_pairs : adjoin(P, forb_pairs)
00463      else found : true),
00464    if not found then return({}) else
00465      return(union(
00466        derived_hitting_cs_pred_forb(adjoin(resolvent_l(C,D,x),setdifference(F,{C,D})),k-1,forb_pairs),
00467        derived_hitting_cs_pred_forb(F,k,adjoin({C,D},forb_pairs)))))$
00468 
00469 monitor_check_dhcpi() := if oklib_monitor then (
00470   print("M[derived_hitting_cs_pred_isoelim]: ENTRY;"),
00471   print("number of steps:", k, "; input clause-set statistics:", statistics_cs(F)))$
00472 monitor_check_dhcpfi_entry() :=
00473  if oklib_monitor and oklib_monitor_level >= 2 then (
00474    print("M[derived_hitting_cs_pred_forb_isoelim]: ENTRY;"),
00475    print("number of steps:", k, "; input clause-set statistics:", statistics_cs(F), "; number of forbidden pairs:", length(forb_pairs)))$
00476 monitor_check_dhcpfi_found() :=
00477  if oklib_monitor and oklib_monitor_level >= 1 then (
00478    print("M[derived_hitting_cs_pred_forb_isoelim]: Found"), print(F))$
00479 
00480 /* The variation where isomorphic cases for branching are eliminated. */
00481 /* Here the predicate can use the derived variables
00482  - P, the resolution pair
00483  - F, the original clause-set.
00484 */
00485 derived_hitting_cs_pred_isoelim(F,k,results_derived_hitting_cs,pred) := (
00486   monitor_check_dhcpi(),
00487   results_derived_hitting_cs :: {},
00488   derived_hitting_cs_pred_forb_isoelim(F,k,{}))$
00489 derived_hitting_cs_pred_forb_isoelim(F,k,forb_pairs) := (
00490  monitor_check_dhcpfi_entry(),
00491  if k < 0 then {}
00492  elseif k = 0 then (
00493    monitor_check_dhcpfi_found(),
00494    results_derived_hitting_cs :: adjoin(F, ev(results_derived_hitting_cs)),
00495    {F})
00496  else
00497  block(
00498   [FP : setdifference(two_subsumption_resolvable_cs(F),forb_pairs),
00499    R,G, found : false, V : var_cs(F)],
00500    for P in FP unless found do (
00501      G : adjoin(resolvent_s(P),setdifference(F,P)),
00502      if not pred(G) then
00503        forb_pairs : adjoin(P, forb_pairs)
00504      else (FP : disjoin(P,FP), found : true, R : P)),
00505    if not found then return({}),
00506    block(
00507     [first_branch : derived_hitting_cs_pred_forb_isoelim(G,k-1,forb_pairs),
00508      removable : {}],
00509      for P in FP do block([G2 : adjoin(resolvent_s(P),setdifference(F,P))],
00510        if is_isomorphic_btr_fcs([V,G],cs_to_fcs(G2)) then
00511          removable : adjoin(P,removable)),
00512     return(union(first_branch,
00513       derived_hitting_cs_pred_forb_isoelim(F,k,adjoin(R,union(forb_pairs,removable))))))))$
00514 
00515 /* The instance of the previous function where no singular variable is
00516    created. */
00517 /* Prerequisite: F does not have singular variables. */
00518 derived_hitting_cs_nsing(F,k,results_derived_hitting_cs) := derived_hitting_cs_pred(F,k,results_derived_hitting_cs,nonsingular_csp)$
00519 derived_hitting_cs_nsing_isoelim(F,k,results_derived_hitting_cs) := derived_hitting_cs_pred_isoelim(F,k,results_derived_hitting_cs,nonsingular_csp)$
00520 
00521 
00522 /* Now computing *all* non-isomorphic cases. repository is a hash table,
00523    and its given value is used. Returns the number of (new) cases found (not
00524    including those already in repository). */
00525 /* The predicate can also use the inherited variables
00526    C,D : parent-clause
00527    x : resolution literal
00528    F : original clause-set.
00529 */
00530 all_derived_hitting_cs_pred_isoelim(F,repository,pred) :=
00531   all_derived_hitting_cs_pred_forb_isoelim(F,{},true)$
00532 /* "repository" and "pred" are inherited. */
00533 /* Uses random_permutation, and is thus governed by set_random_state. */
00534 all_derived_hitting_cs_pred_forb_isoelim(F,forb_pairs,check) := block(
00535  [count : 0, V : var_cs(F)],
00536   oklib_save('repository),
00537   if check then
00538     if not manage_repository_isomorphism_types([V,F], repository) then
00539       return(count)
00540     else count : count + 1,
00541   block(
00542    [FP : setdifference(two_subsumption_resolvable_cs(F),forb_pairs),
00543     R,G, found : false],
00544     for P in random_permutation(FP) unless found do (
00545       G : adjoin(resolvent_s(P),setdifference(F,P)),
00546       if not pred(G) then
00547         forb_pairs : adjoin(P, forb_pairs)
00548        else (FP : disjoin(P,FP), found : true, R : P)),
00549     if not found then return(count),
00550     block(
00551      [removable : {}],
00552       count : count + all_derived_hitting_cs_pred_forb_isoelim(
00553                    G,
00554                    forb_pairs,
00555                    true),
00556       for P in FP do block([G2 : adjoin(resolvent_s(P),setdifference(F,P))],
00557         if is_isomorphic_btr_fcs([V,G],cs_to_fcs(G2)) then
00558           removable : adjoin(P,removable)),
00559       return(count + all_derived_hitting_cs_pred_forb_isoelim(
00560                    F,
00561                    adjoin(R,union(forb_pairs,removable)),
00562                    false)))))$
00563 /* The variation where greedily the min-var-degree is maximised. */
00564 /* Assumes that no variables is eliminated. */
00565 all_derived_hitting_cs_pred_isoelim_mvd(F,repository,pred) :=
00566   all_derived_hitting_cs_pred_forb_isoelim_mvd(F,{},true)$
00567 /* "repository" and "pred" are inherited. */
00568 /* Uses random_permutation, and is thus governed by set_random_state. */
00569 all_derived_hitting_cs_pred_forb_isoelim_mvd(F,forb_pairs,check) := block(
00570  [count : 0, V : var_cs(F), max_mvd],
00571   max_mvd : nonmersenne_rec[deficiency_fcs([V,F]) - 1],
00572   oklib_save('repository),
00573   if check then
00574     if not manage_repository_isomorphism_types([V,F], repository) then
00575       return(count)
00576     else count : count + 1,
00577   block(
00578    [FP : setdifference(two_subsumption_resolvable_cs(F),forb_pairs),
00579     R : {}, G, mvd : minf,
00580     found : false],
00581     for P in random_permutation(FP) unless found do block(
00582       [G2 : adjoin(resolvent_s(P),setdifference(F,P))],
00583       if not pred(G2) then
00584         forb_pairs : adjoin(P, forb_pairs)
00585       else block([d : min_variable_degree_cs(G2)],
00586         if d = max_mvd then (found : true, G : G2, R : P)
00587         else if d > mvd then (mvd : d, G : G2, R : P))
00588     ),
00589     if not found and R = {} then return(count),
00590     block(
00591      [removable : {}],
00592       count : count + all_derived_hitting_cs_pred_forb_isoelim_mvd(
00593                    G,
00594                    forb_pairs,
00595                    true),
00596       FP : setdifference(FP,forb_pairs),
00597       FP : disjoin(R,FP),
00598       for P in FP do block([G2 : adjoin(resolvent_s(P),setdifference(F,P))],
00599         if is_isomorphic_btr_fcs([V,G],cs_to_fcs(G2)) then
00600           removable : adjoin(P,removable)),
00601       return(count + all_derived_hitting_cs_pred_forb_isoelim_mvd(
00602                    F,
00603                    adjoin(R,union(forb_pairs,removable)),
00604                    false)))))$
00605 
00606 /* Now instances and applications of these basic algorithms. */
00607 
00608 /* The instance where no singular variable is created. */
00609 /* Prerequisite: F does not have singular variables. */
00610 all_derived_hitting_cs_nsing_isoelim(F,repository) := all_derived_hitting_cs_pred_isoelim(F,repository,nonsingular_csp)$
00611 all_derived_hitting_cs_nsing_isoelim_mvd(F,repository) := all_derived_hitting_cs_pred_isoelim_mvd(F,repository,nonsingular_csp)$
00612 /* The instance where only resolutions with full parent clauses
00613    are considered. */
00614 all_derived_hitting_cs_fullpc_isoelim(F,repository) := all_derived_hitting_cs_pred_isoelim(F,repository,
00615  lambda([G], nonsingular_csp(G) and is(length(choose_element(P)) = nvar_cs(F))))$
00616 /* The instance without restriction on the 2-subsumption-resolution
00617    steps. */
00618 /* ERROR: Does not work fully correctly, since
00619    all_derived_hitting_cs_pred_isoelim assumes that no variables are
00620    eliminated. */
00621 all_derived_hitting_cs_isoelim(F,repository) := all_derived_hitting_cs_pred_isoelim(F,repository,lambda([G],true))$
00622 
00623 
00624 /* For a given deficiency and number of variables, find all hitting clause-set
00625    types s.t. no singular variables occur.
00626 */
00627 /* The monitoring-variable "results_all_hitting" collects all hitting clause-sets
00628    found (if it has some value, then this will be overwritten). */
00629 all_unsinghitting_def(def,n,results_all_hitting) := (
00630  results_all_hitting :: {},
00631  if def < 1 then {}
00632  elseif def = 1 then if n=0 then results_all_hitting :: {{{}}} else {}
00633  elseif def = 2 and n <= 2 then if n<2 then {} else  results_all_hitting :: {full_fcs(2)[2]}
00634  elseif n <= 2 then {}
00635  else block([F : full_fcs(n)[2]],
00636    if def = 2^n - n then return(results_all_hitting :: {F}),
00637    block([C : setn(n), D : union(setn(n-1),{-n})],
00638      F : adjoin(setn(n-1), setdifference(F,{C,D}))),
00639    representatives_cs(
00640      derived_hitting_cs_nsing_isoelim(F,
00641                               2^n-n-def - 1,
00642                               results_all_hitting))))$
00643 
00644 /* Variation: for a given deficiency and number of 2-subsumption steps,
00645    find all hitting clause-set types s.t. no singular variables occur.
00646 */
00647 all_unsinghitting_steps(steps,n,results_all_hitting) :=
00648   all_unsinghitting_def(2^n-n - steps, n, results_all_hitting)$
00649 
00650 
00651 /* ***********************************************************
00652    * Finding hitting clause-sets with given n systematically *
00653    ***********************************************************
00654 */
00655 
00656 /* For a given number of variables, find all hitting clause-set types
00657    (without singular variables). */
00658 /* Returned is the total number, while parameter hash_repo
00659    (passed by name; initialised empty by this function)
00660    contains the hash-map for all instances. */
00661 /* Prerequisite: n >= 2. */
00662 all_unsinghitting(n, _hash_repo) := block([count],
00663   _hash_repo :: sm2hm({}),
00664   count : all_derived_hitting_cs_nsing_isoelim(full_fcs(n)[2],ev(_hash_repo)),
00665   count
00666 )$
00667 all_unsinghitting_mvd(n, _hash_repo) := block([count],
00668   _hash_repo :: sm2hm({}),
00669   count : all_derived_hitting_cs_nsing_isoelim_mvd(full_fcs(n)[2],ev(_hash_repo)),
00670   count
00671 )$
00672 
00673 
00674 /* ***************************
00675    * Maximal min-var-degrees *
00676    ***************************
00677 */
00678 
00679 /* Late inclusion, since functions above are used by data/uhit_def.mac: */
00680 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def.mac")$
00681 
00682 /* For the uhit-catalogue check for the existence of examples where the
00683    bound minvardegree_dmu(k) is sharp (these have value 0 in the last
00684    component). */
00685 check_uhit_catalogue_maxminvardeg() :=
00686   apply_uhit(lambda([k,n,i,F], [k, n, i, seconde(minvardegree_dmu(k)) - min_variable_degree_cs(F)]))$
00687 /* Extract the [k,n,i]-tuples where the bound is sharp, sorted
00688    lexicographically. */
00689 sharp_uhit_catalogue_maxminvardeg() :=
00690   sort(
00691     map(lambda([t], rest(t,-1)),
00692       sublist(check_uhit_catalogue_maxminvardeg(), lambda([t],is(t[4]=0)))),
00693     orderlessp)$
00694 
00695 /* For given deficiency, compute the maximal min-var-degree (in the
00696    uhit-catalogue). */
00697 max_min_var_deg_uhit_def(k) := max_min_var_deg_cs(ev(all_uhit_def(k),eval))$
00698 max_min_var_deg_uhit_def_mem[k] := max_min_var_deg_cs(ev(all_uhit_def(k),eval))$
00699 /* Apply "remarray(max_min_var_deg_uhit_def_mem)" in case an update
00700    of uhit_def occurred. */
00701 
00702 
00703 /* *************************
00704    * Resolution complexity *
00705    *************************
00706 */
00707 
00708 /* A "nonsingular splitting tree" for a nonsingular unsatisfiable
00709    hitting clause-set F is like an ordinary splitting tree, only
00710    that at each non-root node after the assignment (of a single
00711    variable) singular DP-reduction is applied, until again a
00712    nonsingular (unsatisfiable hitting) clause-set is obtained.
00713    The size of such a tree is, as usual in this context, the
00714    number of leaves; let min_nssplittree_cs(F) be the minimal
00715    possible size.
00716    So the elements of UHIT_{delta=1} have min_nssplittree_cs(F) = 1,
00717    while all other elements have size > 1.
00718 */
00719 
00720 /* For a (valid) isomorphism-type t=[[k,n],i] occurring in uhit_def compute the
00721    minimal size of a nonsingular splitting tree; if a tuple not in the
00722    uhit_def-catalogue is encountered, the tuple together with its type
00723    is printed, and "und" is returned.
00724 */
00725 min_nssplittree_isot[t] := block([k,n,i,F,res:inf,G,tn,sum],
00726  [k,n] : t[1], i : t[2],
00727  if k=1 then return(1),
00728  F : uhit_def[k,n][i],
00729  for v : 1 thru n do (
00730    G : apply_pa_cs({v},F),
00731    tn : redisotype_uhit_def(G),
00732    if tn[2]="new" then (print(G,tn), return(und)),
00733    sum : min_nssplittree_isot[tn],
00734    G : apply_pa_cs({-v},F),
00735    tn : redisotype_uhit_def(G),
00736    if tn[2]="new" then (print(G,tn), return(und)),
00737    sum : sum + min_nssplittree_isot[tn],
00738    res : min(res, sum)
00739  ),
00740  res)$
00741 /* Compute the minimal size of a nonsingular splitting tree for all clause-sets
00742    in uhit_def with deficiency k, sorted by ascending number n of variables,
00743    and then following the order in the uhit-catalogue:
00744 */
00745 min_nssplittree_def(k) := block(
00746  [L : map(first,uhit_def[k,"info"][4]), res : []],
00747   for n in L do block([l : length(uhit_def[k,n])],
00748    for i : 1 thru l do
00749     res : cons(min_nssplittree_isot[[[k,n],i]], res)
00750   ),
00751   reverse(res))$
00752 
00753 
00754 /* ****************************
00755    * Primes and factorisation *
00756    ****************************
00757 */
00758 
00759 /* Decision whether unsatisfiable hitting clause-set F is prime: */
00760 primeuhitting_p(F) := block([c : ncl_cs(F)],
00761  every_s(lambda([P], is(length(hittingdivisor_extension_cs(F,P)) = c)),
00762          powerset(F,2)))$
00763 
00764 
00765