OKlibrary  0.2.1.6
general.hpp File Reference

Plans regarding minimal unsatisfiable clause-sets. More...

Go to the source code of this file.


Detailed Description

Plans regarding minimal unsatisfiable clause-sets.

Todo:
Connections
Todo:
Hitting proof systems
  • See Satisfiability/Lisp/ConflictCombinatorics/HittingProofSystem.mac for first implementations.
  • Likely we should introduce a new submodule; perhaps at base level (i.e., one level up).
  • Regarding stcs2hitref:
    1. Can we extend it, so that it works with extended splitting trees?
    2. Can we characterise when tree hitting clause-sets are being produced?
    3. And can we always find, for appropriate splitting tree, the best hitting refutation?
Todo:
Understanding the recursion for non-Mersenne numbers
  • Understanding the recursion on potential degree-pairs:
    1. In [Kullmann Zhao, 2012] the recursion on potential degree-pairs is introduced.
    2. As a special case we get nonmersenne(k) = nonmersenne_rec3[k]. We should understand this better.
    3. For which k do we have only the "canonical pair" [e,i], i:index_nonmersenne(k), e:nonmersenne(k-i+1), in possible_degree_pairs_nm(k,nonmersenne(k)):
      analyse(k) := block([nm : nonmersenne(k), p],
       p : possible_degree_pairs_nm(k,nm),
       if length(p)=1 then print(k)
      )$
      
      for k : 1 thru 1000 do analyse(k);
      2
      3
      5
      6
      12
      13
      27
      28
      58
      59
      121
      122
      248
      249
      503
      504
           
    4. First case where we have more than one element: k=4.
      possible_degree_pairs_nm(4,6);
        [[[2,4],[3,7,1,6]],[[3,3],[2,7,2,7]]]
           
    5. It seems that we have only the canonical elements precisely for k = 2^m-m and k = 2^m-m+1, for m >= 2.
  • DONE (see [Kullmann Zhao, SAT 2011]) How to prove that nonmersenne_rec[k] and nonmersenne_law(k) in Satisfiability/Lisp/MinimalUnsatisfiability/MinVarDegrees.mac are the same functions?
  • DONE (it is index_nonmersenne_rec(k); (see [Kullmann Zhao, SAT 2011]) Can we determine which i in the recursive formula nm(k) = max_{i in {2,...,k} min(2*i, nm(k-i+1)+i) are relevant?
    1. Analysing the patterns:
      for k : 2 thru 70 do print(k, analyse_nonmersenne_rec(k));
      
      2 [[2,1,"ab"]]
      3 [[3,1,"b"]]
      4 [[3,"a"],[4,1,"b"]]
      5 [[4,2,"ab"]]
      6 [[5,2,"b"]]
      7 [[5,3,"ab"],[6,2,"b"]]
      8 [[6,3,"b"],[7,2,"b"]]
      9 [[6,4,"ab"],[7,3,"b"],[8,2,"b"]]
      10 [[7,4,"b"],[8,3,"b"],[9,2,"b"]]
      11 [[7,"a"],[8,4,"b"],[9,3,"b"],[10,2,"b"]]
      12 [[8,5,"ab"]]
      13 [[9,5,"b"]]
      14 [[9,6,"ab"],[10,5,"b"]]
      15 [[10,6,"b"],[11,5,"b"]]
      16 [[10,7,"ab"],[11,6,"b"],[12,5,"b"]]
      17 [[11,7,"b"],[12,6,"b"],[13,5,"b"]]
      18 [[11,8,"ab"],[12,7,"b"],[13,6,"b"],[14,5,"b"]]
      19 [[12,8,"b"],[13,7,"b"],[14,6,"b"],[15,5,"b"]]
      20 [[12,9,"ab"],[13,8,"b"],[14,7,"b"],[15,6,"b"],[16,5,"b"]]
      21 [[13,9,"b"],[14,8,"b"],[15,7,"b"],[16,6,"b"],[17,5,"b"]]
      22 [[13,10,"ab"],[14,9,"b"],[15,8,"b"],[16,7,"b"],[17,6,"b"],[18,5,"b"]]
      23 [[14,10,"b"],[15,9,"b"],[16,8,"b"],[17,7,"b"],[18,6,"b"],[19,5,"b"]]
      24 [[14,11,"ab"],[15,10,"b"],[16,9,"b"],[17,8,"b"],[18,7,"b"],[19,6,"b"],[20,5,"b"]]
      25 [[15,11,"b"],[16,10,"b"],[17,9,"b"],[18,8,"b"],[19,7,"b"],[20,6,"b"],[21,5,"b"]]
      26 [[15,"a"],[16,11,"b"],[17,10,"b"],[18,9,"b"],[19,8,"b"],[20,7,"b"],[21,6,"b"],[22,5,"b"]]
      27 [[16,12,"ab"]]
      28 [[17,12,"b"]]
      29 [[17,13,"ab"],[18,12,"b"]]
      30 [[18,13,"b"],[19,12,"b"]]
      31 [[18,14,"ab"],[19,13,"b"],[20,12,"b"]]
      32 [[19,14,"b"],[20,13,"b"],[21,12,"b"]]
      33 [[19,15,"ab"],[20,14,"b"],[21,13,"b"],[22,12,"b"]]
      34 [[20,15,"b"],[21,14,"b"],[22,13,"b"],[23,12,"b"]]
      35 [[20,16,"ab"],[21,15,"b"],[22,14,"b"],[23,13,"b"],[24,12,"b"]]
      36 [[21,16,"b"],[22,15,"b"],[23,14,"b"],[24,13,"b"],[25,12,"b"]]
      37 [[21,17,"ab"],[22,16,"b"],[23,15,"b"],[24,14,"b"],[25,13,"b"],[26,12,"b"]]
      38 [[22,17,"b"],[23,16,"b"],[24,15,"b"],[25,14,"b"],[26,13,"b"],[27,12,"b"]]
      39 [[22,18,"ab"],[23,17,"b"],[24,16,"b"],[25,15,"b"],[26,14,"b"],[27,13,"b"],[28,12,"b"]]
      40 [[23,18,"b"],[24,17,"b"],[25,16,"b"],[26,15,"b"],[27,14,"b"],[28,13,"b"],[29,12,"b"]]
      41 [[23,19,"ab"],[24,18,"b"],[25,17,"b"],[26,16,"b"],[27,15,"b"],[28,14,"b"],[29,13,"b"],[30,12,"b"]]
      42 [[24,19,"b"],[25,18,"b"],[26,17,"b"],[27,16,"b"],[28,15,"b"],[29,14,"b"],[30,13,"b"],[31,12,"b"]]
      43 [[24,20,"ab"],[25,19,"b"],[26,18,"b"],[27,17,"b"],[28,16,"b"],[29,15,"b"],[30,14,"b"],[31,13,"b"],
       [32,12,"b"]]
      44 [[25,20,"b"],[26,19,"b"],[27,18,"b"],[28,17,"b"],[29,16,"b"],[30,15,"b"],[31,14,"b"],[32,13,"b"],
       [33,12,"b"]]
      45 [[25,21,"ab"],[26,20,"b"],[27,19,"b"],[28,18,"b"],[29,17,"b"],[30,16,"b"],[31,15,"b"],[32,14,"b"],
       [33,13,"b"],[34,12,"b"]]
      46 [[26,21,"b"],[27,20,"b"],[28,19,"b"],[29,18,"b"],[30,17,"b"],[31,16,"b"],[32,15,"b"],[33,14,"b"],
       [34,13,"b"],[35,12,"b"]]
      47 [[26,22,"ab"],[27,21,"b"],[28,20,"b"],[29,19,"b"],[30,18,"b"],[31,17,"b"],[32,16,"b"],[33,15,"b"],
       [34,14,"b"],[35,13,"b"],[36,12,"b"]]
      48 [[27,22,"b"],[28,21,"b"],[29,20,"b"],[30,19,"b"],[31,18,"b"],[32,17,"b"],[33,16,"b"],[34,15,"b"],
       [35,14,"b"],[36,13,"b"],[37,12,"b"]]
      49 [[27,23,"ab"],[28,22,"b"],[29,21,"b"],[30,20,"b"],[31,19,"b"],[32,18,"b"],[33,17,"b"],[34,16,"b"],
       [35,15,"b"],[36,14,"b"],[37,13,"b"],[38,12,"b"]]
      50 [[28,23,"b"],[29,22,"b"],[30,21,"b"],[31,20,"b"],[32,19,"b"],[33,18,"b"],[34,17,"b"],[35,16,"b"],
       [36,15,"b"],[37,14,"b"],[38,13,"b"],[39,12,"b"]]
      51 [[28,24,"ab"],[29,23,"b"],[30,22,"b"],[31,21,"b"],[32,20,"b"],[33,19,"b"],[34,18,"b"],[35,17,"b"],
       [36,16,"b"],[37,15,"b"],[38,14,"b"],[39,13,"b"],[40,12,"b"]]
      52 [[29,24,"b"],[30,23,"b"],[31,22,"b"],[32,21,"b"],[33,20,"b"],[34,19,"b"],[35,18,"b"],[36,17,"b"],
       [37,16,"b"],[38,15,"b"],[39,14,"b"],[40,13,"b"],[41,12,"b"]]
      53 [[29,25,"ab"],[30,24,"b"],[31,23,"b"],[32,22,"b"],[33,21,"b"],[34,20,"b"],[35,19,"b"],[36,18,"b"],
       [37,17,"b"],[38,16,"b"],[39,15,"b"],[40,14,"b"],[41,13,"b"],[42,12,"b"]]
      54 [[30,25,"b"],[31,24,"b"],[32,23,"b"],[33,22,"b"],[34,21,"b"],[35,20,"b"],[36,19,"b"],[37,18,"b"],
       [38,17,"b"],[39,16,"b"],[40,15,"b"],[41,14,"b"],[42,13,"b"],[43,12,"b"]]
      55 [[30,26,"ab"],[31,25,"b"],[32,24,"b"],[33,23,"b"],[34,22,"b"],[35,21,"b"],[36,20,"b"],[37,19,"b"],
       [38,18,"b"],[39,17,"b"],[40,16,"b"],[41,15,"b"],[42,14,"b"],[43,13,"b"],[44,12,"b"]]
      56 [[31,26,"b"],[32,25,"b"],[33,24,"b"],[34,23,"b"],[35,22,"b"],[36,21,"b"],[37,20,"b"],[38,19,"b"],
       [39,18,"b"],[40,17,"b"],[41,16,"b"],[42,15,"b"],[43,14,"b"],[44,13,"b"],[45,12,"b"]]
      57 [[31,"a"],[32,26,"b"],[33,25,"b"],[34,24,"b"],[35,23,"b"],[36,22,"b"],[37,21,"b"],[38,20,"b"],
       [39,19,"b"],[40,18,"b"],[41,17,"b"],[42,16,"b"],[43,15,"b"],[44,14,"b"],[45,13,"b"],[46,12,"b"]]
      58 [[32,27,"ab"]]
      59 [[33,27,"b"]]
      60 [[33,28,"ab"],[34,27,"b"]]
      61 [[34,28,"b"],[35,27,"b"]]
      62 [[34,29,"ab"],[35,28,"b"],[36,27,"b"]]
      63 [[35,29,"b"],[36,28,"b"],[37,27,"b"]]
      64 [[35,30,"ab"],[36,29,"b"],[37,28,"b"],[38,27,"b"]]
      65 [[36,30,"b"],[37,29,"b"],[38,28,"b"],[39,27,"b"]]
      66 [[36,31,"ab"],[37,30,"b"],[38,29,"b"],[39,28,"b"],[40,27,"b"]]
      67 [[37,31,"b"],[38,30,"b"],[39,29,"b"],[40,28,"b"],[41,27,"b"]]
      68 [[37,32,"ab"],[38,31,"b"],[39,30,"b"],[40,29,"b"],[41,28,"b"],[42,27,"b"]]
      69 [[38,32,"b"],[39,31,"b"],[40,30,"b"],[41,29,"b"],[42,28,"b"],[43,27,"b"]]
      70 [[38,33,"ab"],[39,32,"b"],[40,31,"b"],[41,30,"b"],[42,29,"b"],[43,28,"b"],[44,27,"b"]]
      
           
Todo:
Understanding S_2(k)
  • Printing the values:
    for k : 2 thru 74 do block(
     [i : index_Sma_S2_rec(k)], printf(true, "~2d ~3d ~3d ~2d~%", k, Sma_S2_bydef(k), i, Sma_S2_bydef(i)+i-k-1))$
     2   4   1  0
     3   4   2  2
     4   6   2  1
     5   8   2  0
     6   8   3  0
     7   8   4  2
     8  10   4  1
     9  12   4  0
    10  12   5  2
    11  14   5  1
    12  16   5  0
    13  16   6  0
    14  16   7  0
    15  16   8  2
    16  18   8  1
    17  20   8  0
    18  20   9  2
    19  22   9  1
    20  24   9  0
    21  24  10  0
    22  24  11  2
    23  26  11  1
    24  28  11  0
    25  28  12  2
    26  30  12  1
    27  32  12  0
    28  32  13  0
    29  32  14  0
    30  32  15  0
    31  32  16  2
    32  34  16  1
    33  36  16  0
    34  36  17  2
    35  38  17  1
    36  40  17  0
    37  40  18  0
    38  40  19  2
    39  42  19  1
    40  44  19  0
    41  44  20  2
    42  46  20  1
    43  48  20  0
    44  48  21  0
    45  48  22  0
    46  48  23  2
    47  50  23  1
    48  52  23  0
    49  52  24  2
    50  54  24  1
    51  56  24  0
    52  56  25  0
    53  56  26  2
    54  58  26  1
    55  60  26  0
    56  60  27  2
    57  62  27  1
    58  64  27  0
    59  64  28  0
    60  64  29  0
    61  64  30  0
    62  64  31  0
    63  64  32  2
    64  66  32  1
    65  68  32  0
    66  68  33  2
    67  70  33  1
    68  72  33  0
    69  72  34  0
    70  72  35  2
    71  74  35  1
    72  76  35  0
    73  76  36  2
    74  78  36  1
       
Todo:
Maximal number of MUS's of a clause-set
  • Consider a clause-set F, and let nmus(F) be the number of minimally unsatisfiable clause-sets of F, that is,
    nmus(F) := length(all_min_usat_cores_bydef_cs(F))$
       
  • Sperner's theorem yields nmus(F) <= binom(c(F),c(F)/2). Is this sharp? (Question asked by Joao Marques-Silva, 29.5.2012).
    1. For simplicity consider only even m := c(F).
    2. What is needed is a clause-set F of size m, such that taking any subset of size m/2 we get a minimally unsatisfiable clause-set.
    3. Let's assume that the subsets F' are unsatisfiable hitting clause-set.
      1. Let's further assume that F' is k-uniform.
      2. Then m/2 * 2^(-k) = 1, that is, 2^k = m/2, i.e., k = log_2(m)-1.
      3. Consider thus integer b >= 0, and let m := 2^(b+1), and thus k = b.
      4. Thus we need an unsatisfiable clause-set of size 2^(b+1), where all clauses have size b, and where every subset of size 2^b is hitting.
      5. b <= 1: impossible.
      6. Doesn't seem to exist.

Definition in file general.hpp.