OKlibrary  0.2.1.6
DeficiencyOne.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 19.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2012 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/DataStructures/Lisp/Lists.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Trees/Lisp/Basics.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00027 
00028 
00029 /* We have 
00030  - uniform_usat_hitting_min(k) in 
00031    ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac
00032    for exactly (up to isomorphism) the uniform elements of SMU(1) 
00033    (with 2^k clauses).
00034  - smusat_horn_cs(k) and smusat_horn_stdfcs(k) (also there)
00035    for exactly (up to isomorphism) the Horn elements of SMU(1) (with k
00036    variables).
00037 */
00038 
00039 
00040 /* ************************
00041    * Tree representations *
00042    ************************
00043 */
00044 
00045 /* A "full tree representation" of F in MU(1) is a read-once
00046    resolution tree where every variable of F is resolved
00047    in the whole tree exactly once.
00048    For a "tree representation" the clause-labels are removed,
00049    and only the resolution variables (at inner nodes) and the
00050    clause-labels at the leaves are kept, that is, we have a
00051    binary tree labelled with literals at inner nodes, and with
00052    clauses at leaves.
00053    For tree representations of F in SMU(1) one doesn't need the clauses 
00054    at the leaves, and so splitting trees, where all leaves are labelled by 
00055    "false" and where the variable-labels are unique, are to be used then.
00056 */
00057 
00058 
00059 /* ****************************
00060    * Generating all instances *
00061    ****************************
00062 */
00063 
00064 /* The list of all F in SMU(1) with var(F) = {1,...,n}.
00065    The order is given first by the order of all rooted binary trees,
00066    and then by the lexicographical order of permutations of n (related
00067    to the inner nodes of the tree representations, traversed in in-order).
00068  */
00069 oklib_plain_include("integer_sequence")$
00070 all_smusat1_cs(n) := 
00071  map(treehittingcls_st, map(lambda([P], rt2lrt_il(P[1],P[2],false)),
00072     cartesian_product_l([all2i_rt(n), listify(permutations(1 .. n))])))$
00073 /* The number of these F: */
00074 num_all_smusat1(n) := num_all2i_rt(n) * n!$
00075 
00076 
00077 /* ******************************************************
00078    * Heuristical approach: removing literal occurrences *
00079    * to achieve a given maximal variable degree         *
00080    ******************************************************
00081 */
00082 
00083 /* Auxiliary function */
00084 find_removable_remlitocc(L,x,k) := block(
00085  [occ : sublist_indices(L, lambda([C],elementp(x,C))), deg, locc],
00086   deg : length(occ),
00087   occ : sublist(occ, lambda([i],is(length(L[i]) > k))),
00088   locc : length(occ),
00089   if locc < deg then return([occ, locc]),
00090   block([minl : inf, mini],
00091    for i : 1 thru locc do
00092     if length(L[i]) < minl then (minl : length(L[i]), mini : i),
00093    return([remove_element(mini, occ), locc-1])))$
00094 
00095 /* Input clause-set F (without pure literals, and with min-rank at least k).
00096    Returns [false] if an unsolvable situation was generated, and otherwise a
00097    pair [F',r'], where F' is obtained from F by removal of 
00098    literal-occurrences and r' <= r is the realised maximal var-degree
00099    (maintaining the above invariants throughout). */
00100 remlitocc_greedy(F,k,r) := if F = {} or F = {{}} then [F, minf]
00101  elseif r <= 1 then [false,inf] else block([res : false],
00102  while res = false do (
00103    res : block([degv : max_variable_degree_v_cs(F),
00104       deg,v,dif, L, pocc,lp, nocc,ln, occ],
00105     [deg,v] : degv,
00106     if deg <= r then return([F, deg]),
00107     dif : deg - r,
00108     L : listify(F),
00109     [pocc, lp] : find_removable_remlitocc(L,v,k),
00110     [nocc, ln] : find_removable_remlitocc(L,-v,k),
00111     if lp + ln < dif then return([false,deg]),
00112     occ : append(pocc,nocc),
00113     occ : take_elements(dif, sort(occ, lambda([i,j],ordergreatp(L[i],L[j])))),
00114     for i in occ do
00115       L[i] : setdifference(L[i], {v,-v}),
00116     F : setify(L), return(false))),
00117  return(res))$
00118 
00119 /* Marginal elements of MUSAT(1) (as clause-sets) with 2^k clauses, obtained
00120    from the balanced tree of height k:
00121 */
00122 marginal_musat1(k) := remlitocc_greedy(uniform_usat_hitting_min(k),1,2)[1];
00123