OKlibrary  0.2.1.6
OK_XSZ_min_degree.hpp File Reference

Plans on the joint articles of XSZ and OK. More...

Go to the source code of this file.


Detailed Description

Plans on the joint articles of XSZ and OK.

Todo:
General plans
  • In OK_XSZ_Classification.tex we continuously write a full report, which contains all results we have.
  • The first article shall be OK_XSZ_MinVarDegree.tex, which shall consists (only) of general bound for (minimal) unsatisfiable clause-sets and related material (without considering hitting clause-sets or the classification problems); see "First article" below.
  • The second article contains the upper bound on the min-var-degree for hitting clause-sets (Sections 4, 5, 8.1). The finiteness conjecture is mentioned, but otherwise not discussed.
  • Finally we have a paper on the finitess conjecture and the classification of minimally unsatisfiable clause-sets.
Todo:
DONE (now left/right-overarrows are used, which look somewhat nicer) Is there a better symbol for the min-var-degree?
  • The current symbolism for macro "\minvdeg" uses underlining (for the "minimum", while overlining would be used for "maximum").
  • However, this looks ugly.
  • What else could be used?

    Todo:
    First article
    • This is OK_XSZ_MinVarDegree.tex.
    • DONE (these parts have been written) The content is
      1. Section 6 "The min-var-degree for minimally unsatisfiable clause-sets", and
      2. Section 7 "The min-var-degree for general clause-sets",
      3. plus the parts from Sections 2, 3 not related to hitting clause-sets.
    • Improved bounds:
      1. It would be good if more could be said regarding sharpness of the bounds.
      2. However regarding results involving hitting clause-sets we should only mention later work.
      3. And we should also leave out yet the improvements for general MU; this should go into a separate paper.
    • Questions regarding the sufficient condition for existence of an autarky:
      1. In the context of Corollary 7.4 "min-var-deg(F) > NM(sigma(F)) => F not lean" the Local Lemma is of relevance, and we should investigate the relations.
      2. DONE (OK's conjecture is that this can't be done in poly-time) And, as Remark 1 to Corollary 7.4 asks, it would be good to have an efficient construction for finding the autarky.
    • Generalisations to generalised clause-sets might be difficult, but we should at least discuss the issues.
    • DONE (now part of Theorem 7.2) Open question: bounds on the number of literal occurrences
      1. The problem is, whether Remark 1 to Theorem 7.2 is true, that is, whether there exists a variable v with not only vdg_F(v) <= NM(sigma(F)), but with ldg(v), ldg(-v) <= sigma(F).
    Todo:
    DONE (everything has been transferred resp. generalised) Transfer XSZ's original preprint
    • The title is "The Upper bound of the Fewest Occurrences of Variables in Minimal Unsatisfiable Formulas".
    • Theorem 1 is covered by Theorem 6.3, and also Lemma 1 is.
    • Theorem 2 is covered by Theorem 7.2 (further generalised to arbitrary unsatisfiable clause-sets).
    • Theorem 3 is Lemma 7.3.
    Todo:
    Transfer OK's notes
    • DONE min-var-deg(F) <= 8 for delta(F) = 6
      1. DONE (superseeded by the proof of Lemma 8.3) There exist some notes of OK for a proof.
      2. And from XSZ there is a 2-pages document.
        1. DONE (superseeded by the proof of Lemma 8.3) Lemma 1 shows min-var-deg(F) <= 8.
        2. DONE (captured by Lemma 8.4 now) Lemma 2 generalises this.
      3. DONE (Lemma 8.3) This should go to Section 8.1 in OK_XSZ_Classification.tex.
    Todo:
    Incorporate XSZ new report (from SAT2009)
    • The main result is that a proof of a special case of the general "finiteness conjecture", namely that the maximal number N(k) of variables of non-singular unsatisfiable hitting clause-sets of deficiency k is finite for every k.
    • More specifically, N(3) <= 16.
    • More details on the structure of non-singular unsatisfiable hitting clause-sets F of deficiency 3:
      1. If F contains a full variable, then n(F) <= 7.
      2. The 9 possibilities for such F are listed in the paper.
        1. It is claimed that these are all cases.
        2. Currently we have
          H3 : all_uhit_def(3)$
          length(H3);
            25
                 
          25 unsatisfiable non-singular hitting clause-sets in the catalogue, where 7 contain no full variable, leaving 24-7=18 non-isomorphic cases containing full variables:
          H3f : sublist(H3, lambda([F], full_var_csp(F)));
          [{{-3,-1},{-3,1,2},{-2,-1,3},{-2,1},{-1,2,3},{1,2,3}},
           {{-3,-1},{-3,1},{-2,-1,3},{-2,1,3},{-1,2,3},{1,2,3}},
           {{-3,-2},{-3,-1,2},{-3,1,2},{-2,-1,3},{-2,1,3},{2,3}},
           {{-4,-3},{-4,-1,2,3},{-4,1,2,3},{-3,4},{-2,-1,3},{-2,1,3},{2,3,4}},
           {{-4,-3},{-4,2,3},{-3,-1,4},{-3,1,4},{-2,-1,3},{-2,1,3},{2,3,4}},
           {{-4,-3,-2},{-4,-2,3},{-3,-2,-1,4},{-3,-2,1,4},{-2,3,4},{-1,2},{1,2}},
           {{-4,-3,-1},{-4,-3,1,2},{-4,-2,-1,3},{-4,-2,1},{-4,2,3},{-3,4},{3,4}},
           {{-4,-3},{-4,-2,-1,3},{-4,-2,1,3},{-4,-1,2,3},{-4,1,2,3},{-3,4},{3,4}},
           {{-5,-4,-3},{-5,-4,3},{-5,-3,4},{-5,3,4},{-2,-1,5},{-2,1,5},{-1,2,5},{1,2,5}},
           {{-5,-4,-2},{-5,-3,2},{-4,-2,5},{-3,2,5},{-2,-1,4},{-2,1,4},{-1,2,3},{1,2,3}},
           {{-5,-4,-2},{-5,-2,3,4},{-4,-3,-2,5},{-3,-2,-1,4},{-3,-2,1,4},{-2,3,5},{-1,2},{1,2}},
           {{-5,-4},{-5,4},{-4,5},{-3,-2,-1,4,5},{-3,1,4,5},{-2,3,4,5},{-1,2,4,5},{1,2,3,4,5}},
           {{-5,-4},{-5,4},{-4,-3,5},{-3,4,5},{-2,-1,3,5},{-2,1,3,5},{-1,2,3,5},{1,2,3,5}},
           {{-5,-4},{-5,4},{-4,-2,-1,3,5},{-3,-2,5},{-3,1,2,5},{-2,-1,3,4,5},{-1,2,5},{1,3,5}},
           {{-5,-4},{-5,4},{-4,-1,3,5},{-3,-2,5},{-3,2,5},{-2,1,3,5},{-1,3,4,5},{1,2,3,5}},
           {{-6,-5,-4,-3},{-6,-5,3},{-6,-4,5},{-6,-3,4},{-6,3,4,5},{-2,-1,6},{-2,1,6},{-1,2,6},{1,2,6}},
           {{-6,-1},{-6,1},{-5,-4,-3,-2,6},{-5,-4,2,6},{-4,-3,5,6},{-4,-2,3,6},{-4,2,3,5,6},{-1,4,6},{1,4,6}},
           {{-7,-6,-5,-4},{-7,-6,4},{-7,-5,6},{-7,-4,5},{-7,4,5,6},{-3,-2,-1,7},{-3,1,7},{-2,3,7},{-1,2,7},{1,2,3,7}}]
                 
        3. These 18 clause-sets are exactly those given by the 9 cases in the paper:
          X1(F1,F2) := fcs2cs(full_gluing(cs2fcs(F1),cs2fcs(F2)))$
          L1 : lappend(outermap(X1, 
            all_smusat1_cs(2), 
            all_smusat1_cs(2)))$
          nvar_cs(first(L1));
            3
          setify(map(second,classify_candidates_uhit_def(L1)));
            {1,2,3}
          
          X2(F1,F2) := fcs2cs(full_gluing(cs2fcs(F1),cs2fcs(F2)))$
          L2 : lappend(outermap(X2, 
            all_smusat1_cs(2),
            sublist(all_smusat1_cs(3), lambda([F], is(singular_variables_cs(F) = {1,2})))));
          nvar_cs(first(L2));
            4
          setify(map(second,classify_candidates_uhit_def(L2)));
            {5}
          
          X3(FF) := full_gluing(FF, [{1},{{-1},{1}}])$
          L3 : map(fcs2cs,map(X3, 
            sublist(listify(all_uhitd2_fcs(3)), lambda([FF], subsetp(singular_variables_fcs(FF),{1})))));
          nvar_cs(first(L3));
            4
          setify(map(second,classify_candidates_uhit_def(L3)));
            {2,6,8,10}
          
          X4(F1,F2) := fcs2cs(full_gluing(cs2fcs(F1),cs2fcs(F2)))$
          L4 : lappend(outermap(X2, 
            sublist(all_smusat1_cs(3), lambda([F], is(singular_variables_cs(F) = {1,2}))),
            sublist(map(lambda([F],rename_cs(F,[1,2,4])),all_smusat1_cs(3)), lambda([F], is(singular_variables_cs(F) = {1,2})))));
          nvar_cs(first(L4));
            5
          setify(map(second,classify_candidates_uhit_def(L4)));
            {2}
          
          X5(FF) := full_gluing(FF, [{1},{{-1},{1}}])$
          L5 : map(fcs2cs,map(X5, 
            sublist(listify(all_uhitd2_fcs(4)), lambda([FF], is(singular_variables_fcs(FF) = {1})))))$
          length(L5);
            86
          nvar_cs(first(L5));
            5
          setify(map(second,classify_candidates_uhit_def(L5)));
            {3,5,7,8,9}
          
          L6 : [fcs2cs(vardisjoint_full_gluing(musatd2(2),musatd2(2)))];
          nvar_cs(first(L6));
            5
          setify(map(second,classify_candidates_uhit_def(L6)));
            {1}
          
          U5 : all_reps_uhitd2_fcs(5)$
          length(U5);
            47;
          map(singular_variables_fcs,U5);
            {{3,4,5},{3,5},{4,5},{5}}
          U5s : subset(U5, lambda([FF], is(singular_variables_fcs(FF)={5})));
            {[{1,2,3,4,5},{{-5,4},{-4,-3,-2,-1},{-4,-3,1},{-4,-2,3},{-4,-1,2},{-4,1,2,3},{4,5}}]}
          L7a : [rename_fcs(single_element(U5s),[5,2,3,4,1])];
            [[{1,2,3,4,5},{{-5,-4,-3,-2},{-5,-4,2},{-4,-3,5},{-4,-2,3},{-4,2,3,5},{-1,4},{1,4}}]]
          X7(FF) := full_gluing(FF, [{1},{{-1},{1}}])$
          L7 : map(fcs2cs,map(X7, L7a));
          nvar_cs(first(L7));
            6
          setify(map(second,classify_candidates_uhit_def(L7)));
            {2}
          
          L8 : [fcs2cs(vardisjoint_full_gluing(musatd2(2),musatd2(3)))];
          nvar_cs(first(L8));
            6
          setify(map(second,classify_candidates_uhit_def(L8)));
            {1}
          
          L9 : [fcs2cs(vardisjoint_full_gluing(musatd2(3),musatd2(3)))];
          nvar_cs(first(L9));
            7
          setify(map(second,classify_candidates_uhit_def(L9)));
            {1}
                 
          where the clause-set from case 7 was added to the catalogue.
      3. For F without full variables, three examples are given in the paper, constructed b the following "special" function.
        BF : musatd2(3);
        /* 1 <= i < j <= 5: */
        sp_uhitdef3(i,j) := block([BF : musatd2(3)[2], C1, C2],
          C1 : listify(BF)[i], C2 : listify(BF)[j],
          union(setdifference(BF, {C1,C2}), {adjoin(4,C1), adjoin(-4,C1), adjoin(4,C2), adjoin(-4,C2)}))$
        L : create_list(sp_uhitdef3(i,j), i,1,4,j,i+1,5)$
        check(F) := not emptyp(check_hitting_nsing_def(F)) and not full_var_csp(F)$
        every_s(check,L);
        (%i32) map(second,classify_candidates_uhit_def(L));
          [1,1,1,9,7,7,1,7,1,1]
            
        So they are all already in the catalogue.
      4. In the hitting catalogue of the OKlibrary we have 7 different examples of such F:
        H3 : all_uhit_def(3)$
        H3n : sublist(H3, lambda([F], not full_var_csp(F)));
         [{{-4,-3},{-4,-1,2,3},{-4,1,2,3},{-3,-2,4},{-2,-1,3},{-2,1,3},{2,4}},
         {{-4,-3},{-4,-1,2,3},{-4,1,3},{-3,-2,-1,4},{-2,-1,3},{-2,1,4},{2,4}},
         {{-4,-3},{-4,2,3},{-3,-2,1,4},{-3,-1,4},{-2,3},{-1,2,3,4},{1,2,4}},
         {{-4,-3,-2},{-4,2},{-3,-1,4},{-3,1,4},{-2,-1,3},{-2,1,3},{2,3,4}},
         {{-4,-3,-2,-1},{-4,1,2,3},{-3,-2,-1,4},{-3,1},{-2,3},{-1,2},{1,2,3,4}},
         {{-5,-4,-2,-1},{-5,-4,-2,1},{-5,-2,-1,4},{-5,-2,1,4},{-5,2,3},{-3,-2,5},{-3,2},{3,5}},
         {{-5,-4},{-5,-3,4},{-4,-2,-1,3,5},{-4,-2,1,3,5},{-4,-1,2,3,5},{-4,1,2,3,5},{-3,5},{3,4}}]
        map(second,classify_candidates_uhit_def(H3n));
         [1,3,4,7,9,4,6]
            
      5. So XSZ's examples have indices 1, 4, 5 in H3n. while indices 2,3,6,7 contain new examples; these are
         {{-4,-3},{-4,-1,2,3},{-4,1,3},{-3,-2,-1,4},{-2,-1,3},{-2,1,4},{2,4}},
         {{-4,-3},{-4,2,3},{-3,-2,1,4},{-3,-1,4},{-2,3},{-1,2,3,4},{1,2,4}},
         {{-5,-4,-2,-1},{-5,-4,-2,1},{-5,-2,-1,4},{-5,-2,1,4},{-5,2,3},{-3,-2,5},{-3,2},{3,5}},
         {{-5,-4},{-5,-3,4},{-4,-2,-1,3,5},{-4,-2,1,3,5},{-4,-1,2,3,5},{-4,1,2,3,5},{-3,5},{3,4}}]
             
      6. If the above is everything, then actually N(3) would be 7.
    • Before Lemma 1, everything should already be in the report.

Definition in file OK_XSZ_min_degree.hpp.