OKlibrary  0.2.1.6
MaximiseMinVarDegrees.hpp File Reference

Plans on investigations into the maximum of the min-var-degree of parameterised classes of unsatisfiable clause-sets. More...

Go to the source code of this file.


Detailed Description

Plans on investigations into the maximum of the min-var-degree of parameterised classes of unsatisfiable clause-sets.

Todo:
Minimally unsatisfiable clause-sets
Todo:
Unsatisfiable non-singular hitting clause-sets
  • See Satisfiability/Lisp/MinimalUnsatisfiability/MinVarDegrees.mac.
  • And see Satisfiability/Lisp/MinimalUnsatisfiability/plans/MinVarDegrees.hpp.
  • The function "sharp_uhit_catalogue_maxminvardeg" investigates the catalogue for the sharp cases w.r.t. the general upper bound minvardegree_dmu (w.r.t. deficiency, for MU).
  • n-oriented investigations:
    1. One tool is e.g. "all_unsinghitting(5, 'all_n5)" and "all_unsinghitting_mvd(5, 'all_n5)" for searching through all cases for n=5.
    2. And then applying e.g. "d_all_n5 : analyse_isorepo_defset_mvd(all_n5)" to get the sharp cases obtained.
    3. While by "d_all_n5 : analyse_isorepo_defset_imprmvd(all_n5)" we get the cases which improve upon the catalogue; this belongs more to the "deficiency-oriented investigations" below.
    4. However in this way it seems very unlikely to get sharp examples for deficiencies much smaller than the gap-deficiencies.
    5. While determining the possible distribution of clause-lengths due to the condition sum_C 2^(-|C|) = 1 by all_cld_uhit_maxminvd and then either determining that there are no examples for the given n, or constructing them by hand seems to be more successful.
    6. See "all_cld_uhit_minvd" in ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/plans/HittingClauseSets.hpp for further strengthenings of this approach (especially regarding the use of (generalised) SAT solving).
    7. We know that the bound nonmersenne is sharp for given n and deficiencies k = 2^n-n - i for 0 <= i <= n.
    8. For n <= 3 this cannot be applied fully, and there we also have full information.
    9. For n=4 we have the sharp cases k = 12,11,10,9,8,7,6,4,3 in the catalogue. This information is complete.
    10. n = 5:
      1. The sharp cases in the catalogue are k = 27,26,25,24,23,22,21,20, 19,18,13,4.
      2. For k = 17 we have all_cld_uhit_maxminvd(k,5) = {{[2,1],[3,1],[5,20]}}, thus there exists a variable not occurring in the first two clauses, and thus occurring only 22 - 2 = 20 < 21 times, so here there is no sharp case.
      3. For k = 14,15,16 due to all_cld_uhit_maxminvd(k,5) = {} we know there are no sharp cases.
      4. For k = 12 we have all_cld_uhit_maxminvd(k,5) = {{[1,1],[5,16]}}, and so there is no non-singular sharp case.
      5. k = 11 ?
      6. k = 10 ?
      7. k = 9 ?
      8. k = 8 ?
      9. k = 7 ?
      10. For k = 6 we have the only the non-singular case {{[2,3],[5,8]}}, and so there is a variable not occurring in the first three clauses, thus occurring 11 - 3 = 8 < 9 time, so we might have a sharp case.
      11. For k = 5 the only non-singular case is {[2,3],[4,1],[5,6]}}, so again in variable is not occurring in the first three clauses, thus occurring 10 - 3 = 7 < 8 times, so no sharp case here.
      12. For k = 3 the non-singular cases are
        • {[2,1],[3,5],[4,2]} ?
        • {[2,2],[3,2],[4,4]} ?
        • {[2,2],[3,3],[4,1],[5,2]} ?
        • {[2,3],[3,1],[5,4]} ?
        • {[2,3],[4,3],[5,2]} ?
    11. For n=6 we only have incomplete information.
      1. The general cases for sharpness are k = 58, 56,55,54,53,52,51.
      2. And then we have sporadic cases for k = 43.
      3. We should also get all min-var-degree-maximal cases into the catalogue, but likely only optionally.
      4. For 14 <= k <= 19 we have all_cld_uhit_maxminvd_nu(13,6)={}, and so we do not have sharp cases here.
      5. k = 13: all_cld_uhit_maxminvd_nu(13,6)={{[2,3],[6,16]}}, where the first 3 binary clauses must leave out one variable, which then occurs 19 - 3 = 16 < 17 times, so we might have a sharp case here.
      6. k = 6: all_cld_uhit_maxminvd_nu(6,6) has the following cases:
        • {[2,2],[3,3],[5,1],[6,6]}: Impossible, since a hitting cls consisting of two binary and two ternary clauses can contain at most 5 variables.
        • {[2,3],[3,1],[6,8]}: Possible, since the first three clauses can involve only 3 variables, so the first four clauses can only involve 5 variables, thus one variable has occurrence 12 - 4 = 8 < 9.
        • {[2,3],[4,1],[5,4],[6,4]}: Impossible, since the first three clauses only involve 3 variables, so the fourth clause only can contain one of them, so this literal must provide the clash with the first three clauses, which is not possible.
        • {[2,3],[4,2],[5,1],[6,6]}: Impossible, since the fourth clause can only introduce 2 new variables, leaving one variable not occurring four times.
    12. For n=7 we only have incomplete information.
      1. The general cases for sharpness are k = 121, 120,119,118,117,116,115,114.
      2. k = 17 : all_cld_uhit_maxminvd_nu(17,7) = {{[2,3],[4,1],[5,1],[6,1],[7,18]}}: The first three clauses can only use 3 variables, so the first four clauses leave out one variable, which then occurs 24 - 4 = 20 < 21 times. So no sharp case here.
      3. For k = 15,16 we have all_cld_uhit_maxminvd_nu(k,7)={}, and so we do not have sharp cases here.
      4. k = 14 : all_cld_uhit_maxminvd_nu(14,7)={{[2,3],[4,2],[7,16]}}. The first three clauses can only use 3 variables, so the first four clauses leave out one variable, which then occurs 21 - 4 = 17 < 18 times. So no sharp case here.
      5. k = 13: all_cld_uhit_maxminvd_nu(13,7)={{[2,3],[3,1],[7,16]}}. Now a hitting cls F with c(F) = 3 which is 2-uniform has n(F) <= 3, and thus the first 4 clauses must leave out one variable, which then occurs 20 - 4 = 16 < 17 times. So possibly a sharp case here.
      6. k = 6: The cases of all_cld_uhit_maxminvd_nu(6,7) are as follows.
        • Every variable can loose at most 4 occurrences.
        • {[2,2],[3,3],[4,1],[6,1],[7,6]}: Impossible.
        • {[2,2],[3,3],[5,2],[6,2],[7,4]}: Impossible for the same reason.
        • {[2,3],[3,1],[4,1],[7,8]}: Impossible, like the following case.
        • {[2,3],[3,1],[5,1],[6,4],[7,4]}: Possible, since the first four clauses can only contain 4 variables (see below), so the fifth clause must contain all other 3 variables, and two of literals are furthermore fixed for the clash with the first three clauses, which, since this is the same for the fourth clause, doesn't leave a conflict with the fourth clause. So 13 - 5 = 8 < 9.
        • {[2,3],[3,1],[5,2],[6,1],[7,6]}: Possible as the previous case.
        • {[2,3],[3,1],[6,7],[7,2]}
        • {[2,3],[4,1],[5,5],[7,4]}
        • {[2,3],[4,2],[5,1],[6,5],[7,2]}
        • {[2,3],[4,2],[5,2],[6,2],[7,4]}
        • {[2,3],[4,3],[6,1],[7,6]}
        A general principle:
        • If hitting F consists of 3 binary variables, then the only cases are
          1. A : {{a,b},{-a,b},{-b,a}}
          2. B : {{a,b},{-a,c},{-a,-c}}
          3. C : {{a,b},{-a,c},{-b,-c}}
          and every other clause must contain two of these variables to produce a clash (in case of case C it must contain all three, while in case A it must contain {-a,-b}, and in case B it must contain {a,-b}).
        • This follows from the fact that the sub-clause-set consisting of these four clauses is hitting, and we can remove all pure literals, so only the three variables involved are of relevance.
        • Every hitting cls has sum_C 2^(-|C|) <= 1, thus the last clause must then be binary.
        • And this last clause is then also unique (since only one satisfying assignment is left).
    13. For n=8 we only have incomplete information.
      1. The general cases for sharpness are k = 248, 247,246,245,244,243,242,241,240.
      2. k = 14: all_cld_uhit_maxminvd_nu(14,8) has the following cases:
        • {[2,2],[3,3],[4,1],[8,16]}: Impossible since the first five clauses cannot contain all 8 variables XXX.
        • {[2,3],[3,1],[5,1],[6,1],[7,4],[8,12]}: Impossible, since the first five clauses can only use 4+3=7 variables, so one variable occurs 22-5=17 < 18 times.
        • {[2,3],[3,1],[5,1],[6,2],[7,1],[8,14]}: Impossible by the same reason.
        • {[2,3],[3,1],[5,2],[8,16]}: Again impossible.
        • {[2,3],[4,3],[8,16]}: Impossible, since the first 5 clauses can only use 3 + 2*2 = 7 variables.
        So no sharp case here.
      3. k = 13: all_cld_uhit_maxminvd_nu(13,8) has the following cases:
        • {[2,2],[3,3],[4,1],[7,1],[8,14]}
        • [2,3],[3,1],[4,1],[8,16]}
        • {[2,3],[3,1],[5,1],[6,2],[7,2],[8,12]}
        • {[2,3],[3,1],[5,2],[7,1],[8,14]}
        • {[2,3],[4,3],[7,1],[8,14]}}
        The first cases look impossible, perhaps the last one might be possible.
    14. n=9
      1. k = 14: all_cld_uhit_maxminvd_nu(14,9) has the following prefix-cases:
        1. [2,2],[3,3],[4,1]
        2. [2,2],[3,3],[5,3]
        3. [2,3],[3,1],[4,1],[6,1]
        4. [2,3],[3,1],[4,1],[7,1]
        5. [2,3],[3,1],[5,1],[6,4]
        6. [2,3],[3,1],[5,2]
        7. [2,3],[4,3]
        It might be that all these hitting clause-sets with 6 clauses can contain only 8 variables (at most), and thus one variable has only 23 - 6 = 17 < 18 occurrences.
      2. We need some general methods to establish upper bounds on n(F) for hitting cls F with given list of clause-lengths.
  • Deficiency-oriented investigations:
    1. max_min_var_deg_uhit_def(k) yields the maximal min-var-deg realised in the uhit_def-catalogue for deficiency k.
    2. For 1 <= k <= 59 sharpness of the bound is not known for 14 <= k <= 17, 29 <= k <= 42 and 44 <= k <= 51.
    3. We have the current maxima for the non-sharp cases (compared to the upper bound minvardegree_dmu; use sharp_uhit_catalogue_maxminvardeg()):
      • k = 15 : 18 = 19-1
        1. The above show that for a sharp case we have n >= 8.
      • k = 16 : 19 = 20-1
        1. The above show that for a sharp case we have n >= 8.
      • k = 17 : 20 = 21-1
        1. The above show that for a sharp case we have n >= 8.

Definition in file MaximiseMinVarDegrees.hpp.