OKlibrary  0.2.1.6
general.hpp File Reference

On investigations regarding categories of clause-sets. More...

Go to the source code of this file.


Detailed Description

On investigations regarding categories of clause-sets.

Todo:
Links
Todo:
Satisfiability of products
  • The first form of the conjecture (falsified below) is that for a finite family of unsatisfiable flcls's, none of them containing the empty clause, their product is unsatisfiable as well.
  • Considering the product of full clause-sets V_n:
    prl(L) := product_flcls(map(fcls2flcls, map(full_fcs,L)))$
    prlfcs(L) := flcls2fcls(prl(L))$
    testl(L) := current_satsolver(prlfcs(L))$
    
    testl([0,0]);
      false;
    testl([0,1]);
      true;
    testl([1,1]);
      false;
    testl([1,2]);
      true;
    testl([1,3]);
      true;
    testl([1,4]);
      true;
    testl([1,5]);
      true;
    testl([1,6]);
      true;
    
    prl([1,2]);
    [
      [{[-1,-2],[-1,-1],[-1,1],[-1,2],[1,-2],[1,-1],[1,1],[1,2]},
       lambda([x],map('apply,[lambda([x],-x),lambda([x],-x)],map("[",x)))],
      {{[-1,-2],[-1,-1]},{[-1,-2],[-1,1]},{[-1,-1],[-1,2]},{[-1,1],[-1,2]},
      {[1,-2],[1,-1]},{[1,-2],[1,1]},{[1,-1],[1,2]},{[1,1],[1,2]}}
    ]
    flcls2fcls(prl([1,2]));
      [{1,2,3,4},{{-4,-3},{-4,-2},{-3,-1},{-2,-1},{1,2},{1,3},{2,4},{3,4}}]
    all_sat_fcs(flcls2fcls(prl([1,2])));
      {{-4,-1,2,3},{-3,-2,1,4}}
    % Solutions interpreted:
    [1,1],[1,-1],[-1,2],[-1,-2]
    -2,-3,4,1
    [-1,-1],[-1,1],[1,-2],[1,2]
    2,3,-4,-1
    
    length(all_sat_fcs(flcls2fcls(prl([1,2]))));
      2
    length(all_sat_fcs(flcls2fcls(prl([1,3]))));
      18
    length(all_sat_fcs(flcls2fcls(prl([1,4]))));
      110
    length(all_sat_fcs(flcls2fcls(prl([1,5]))));
      570
    length(all_sat_fcs(flcls2fcls(prl([1,6]))));
      2702
    length(all_sat_fcs(flcls2fcls(prl([1,7]))));
      12138
    
    map(factor,[2,18,110,570,2702]);
      [2, 2*3^2, 2*5*11, 2*3*5*19, 2*7*193]
    eis_search(2,18,110,570,2702);
      ["A038721"]
    eis_search_name(2,18,110,570,2702);
      A038721 - k=2 column of A038719.
    eis_search(1,9,55,285,1351);
      ["A016269"]
    eis_search_name(1,9,55,285,1351);
    A016269 - Number of monotone Boolean functions of n variables with 2 mincuts. 
    Also number of Sperner systems with 2 blocks.
    
    eis_details(A016269);
    
    A016269 - Number of monotone Boolean functions of n variables with 2 mincuts. 
    Also number of Sperner systems with 2 blocks.
    
    UNSIGNED TERMS
      1, 9, 55, 285, 1351, 6069, 26335, 111645, 465751, 1921029, 7859215, 
      31964205, 129442951,522538389, 2104469695, 8460859965, 33972448951, 
      136276954149, 546269553775, 2188563950925, 8764714059751
    
    OFFSET
      0, 2
    
    FORMULA
      G.f.: 1/((1-2x)(1-3x)(1-4x)). a(n) = (2^n)*(2^n - 1)/2 - 3^n + 2^n.
      a(n)=sum{0<=i,j,k,<=n, i+j+k=n, 2^i*3^j*4^k}. - Hieronymus Fischer 
       (Hieronymus.Fischer(AT)gmx.de), Jun 25 2007
      a(n)=2^(n+1)*(1+2^(n+2))-3^(n+2). - Hieronymus Fischer 
       (Hieronymus.Fischer(AT)gmx.de), Jun 25 2007
      a(n) = 3*StirlingS2(n+1,4) + StirlingS2(n+1,3). - Ross La Haye 
       (rlahaye(AT)new.rr.com), Jan 10 2008
    
    MAPLE PROGRAM
      with(combinat):a:=n->stirling2(n,4)-stirling2(n-1,4): seq(a(n), n=4..24); 
      - Zerinvary Lajos (zerinvarylajos(AT)yahoo.com), Oct 05 2007
    
    CROSS-REFERENCES
      Equals (1/2) A038721(n+1). First differences of A000453. 
      Partial sums of A027650.
      Pairwise sums of A099110.
      Odd part of A019333. Cf. A000392, A032263.
      Adjacent sequences: A016266 A016267 A016268 this_sequence A016270 A016271 
        A016272
      Sequence in context: A058852 A068970 A141530 this_sequence A005770 A030053 
        A072844
    
    REFERENCES
      L. Comtet, Advanced Combinatorics, Reidel, 1974, p. 292, #8, s(n,2).
    
    HYPERLINKS
      K. S. Brown, Dedekind's problem [http://www.mathpages.com/home/kmath030.htm]
      Vladeta Jovovic, Illustration for A016269, A047707, A051112-A051118
    [http://www.research.att.com/~njas/sequences/a047707.pdf]
      Index entries for sequences related to Boolean functions
    [http://www.research.att.com/~njas/sequences/Sindx_Bo.html#Boolean]
      Goran Kilibarda and Vladeta Jovovic, Antichains of Multisets
    [http://www.cs.uwaterloo.ca/journals/JIS/index.html], J. Integer Seqs., 
      Vol. 7, 2004.
    
    COMMENTS
      Half the number of 2 X (n+2) binary arrays with both a path of adjacent 1's 
      and a path of adjacent 0's from top row to bottom row. 
        - Ron Hardin (rhh(AT)cadence.com), Mar 21 2002
      As (0,0,1,9,55,...) this is the third binomial transform of cosh(x)-1. 
      It is the binomial transform of A000392, when this has two leading zeros. 
      Its e.g.f. is then exp(3x)cosh(x)-exp(3x) and a(n)=(4^n-2*3^n+2^n)/2. 
        - Paul Barry (pbarry(AT)wit.ie), May 13 2003
      Let P(A) be the power set of an n-element set A. Then a(n-2) = the number of
      pairs of elements {x,y} of P(A) for which either 
       0) x and y are disjoint and for which x is not a subset of y and y is
          not a subset of x, or 
       1) x and y are intersecting but for which x is not a subset of y and y is 
          not a subset of x. - Ross La Haye (rlahaye(AT)new.rr.com), Jan 10 2008
    
    testl(2,2);
      false;
    testl(2,3);
      false;
    testl(3,3);
      false;
    
    testl([2,2,2]);
      false;
    testl([2,2,3]);
      false;
    
    testl([2,2,2,2]);
    
       
    Below we will see that a(n) should start with 0 (for n=1), that is, the sequence should be right-shifted, with a 0 added at the beginning.
  • Investigation of prl([1,n]):
    1. Let F_n := prl([1,n]) = V_1 x V_n and s_n := length(all_sat_fcs(flcls2fcls(prl([1,n])))) the number of satisfying assignments of F_n.
    2. And let a(n) be sequence A016269, and thus s_n = 2*a(n-1).
    3. F_n is complementation-invariant (as a product of complementation- invariant clause-sets) and bipartite (as every product V_1 x V is: one part is given by {1} x V_n, the other by {-1} x V_n):
      map(bipartite_fcs_p,create_list(prlfcs([1,n]),n,1,5));
        [true,true,true,true,true]
      
      map(lambda([FF], is(comp_fcs(FF) = FF)), create_list(prlfcs([1,n]),n,1,5));
        [true,true,true,true,true]
           
    4. Thus we actually have a hypergraph 2-colouring problem, namely the problem of 2-colouring the hypergraph G_n := cls2hg(V_n) (with the 2n literals as vertices).
      is_isomorphic_btr_fcs(tcol2sat_hg2fcs(fcs2hg(full_fcs(1))), prlfcs([1,1]));
        true
      is_isomorphic_btr_fcs(tcol2sat_hg2fcs(fcs2hg(full_fcs(2))), prlfcs([1,2]));
        true
      is_isomorphic_btr_fcs(tcol2sat_hg2fcs(fcs2hg(full_fcs(3))), prlfcs([1,3]));
        true
      is_isomorphic_btr_fcs(tcol2sat_hg2fcs(fcs2hg(full_fcs(4))), prlfcs([1,4]));
        true
      is_isomorphic_btr_fcs(tcol2sat_hg2fcs(fcs2hg(full_fcs(5))), prlfcs([1,5]));
        true
           
    5. Now it is easy to see that F_n for n >= 2 is satisfiable, since G_n is obviously 2-colourable: Give the vertices -1,+1 colour 1, and give vertices -2,+2 colour 2 --- every hyperedge contains -1 or +1, and every hyperedge contains -2 or +2.
    6. It remains to determine s_n, the number of 2-colourings of G_n.
    7. The 2-colourings of G_n are the partitions of {-n,...,n} - {0} such that no part contains a hyperedge of G_n; these are exactly the partitions such that each part contains both i,-i for some i.
    8. So the 2-colourings of G_n correspond to triples (A,B,x), where A,B are disjoint subsets of {1,...,n}, while x is a vector with entries -1,+1 of length n - |A| - |B| : for i in A the vertices i,-i get colour 1, for i in B the vertices i,-i get colour 2, and x determines for the remaining vertices whether the positive or the negative vertex gets colour 1 resp. colour 2.
      alldisjnepairs(n) := second(kneser_g_hg(ses2hg(disjoin({},powerset(setn(n))))));
      an_v1(n) := sum_l(map(
        lambda([P], 2^(n-length(first(P))-length(second(P)))),
        listify(alldisjnepairs(n))));
      
      create_list(an_v1(n),n,1,6);
        [0,1,9,55,285,1351]
           
      an_v1(n) = a(n-1) = 1/2 s_n; note that an_v1(n) computes only half of the assignments, since only one form of a pair (A,B) is considered.
    9. "Also number of Sperner systems with 2 blocks." in A016269 means the number of subsumption-free hypergraphs with n+1 vertices not containing the empty hyperedge:
      all_Sp_2bl(n) := subset(powerset(powerset(setn(n)), 2), lambda([S], 
          is(length(S)=2) and not elementp({},S) and is_antichain(S)))$
      an_v2(n) := length(all_Sp_2bl(n))$
      
      create_list(an_v2(n),n,1,6);
        [0,1,9,55,285,1351]
           
    10. So s_n = 1/2 * number of Sperner systems with n vertices and 2 blocks.
    11. This is proven as follows:
      1. We have to show an_v2(n) = an_v1(n).
      2. This is done be constructing a bijection between all triples (A,B,x) as specified above and the two-element subsumption-free pairs (X,Y) of the powerset of {1,..,n}.
      3. To (A,B,X) we assign (X,Y), where X := A + C, Y := B + C, and where C is the set of i in X - (A+B) with value +1 at the corresponding position in x.
    12. A formula for s_n/2 is as follows:
      an_v3(n) := binomial(2^n,1) + binomial(2^n,2) - 3^n;
      create_list(an_v3(n),n,1,10);
        [0,1,9,55,285,1351,6069,26335,111645,465751]
           
      which is shown as follows:
      1. The number of all anti-chains {A,B}, where A,B are subsets of {1,...,n}, is to be computed.
      2. The number of all subsets {A,B} (possibly A=B) is binomial(2^n,1) + binomial(2^n,2).
      3. From this we have to subtract the number of all {A,B} where A <= B or B <= A.
      4. These sets can be mapped bijectively to all pairs (A,B) with A <= B <= {1,...,n} by sorting.
      5. Now these pairs exactly represent the partial assignment over {1,...,n}, where elements in A are unassigned, elements in B-A are positive, elements in {1,...,n}-B are negative.
  • So perhaps unit-clauses are also problematic, not just empty clauses?
  • For the special case of products of full clauses, the conjecture is that testl(L) yields true iff L contains a 0 and a non-0 or a 1 and a non-1.
  • The new conjecture for the general case then could be: A product of literal-based formal clause-sets, where all clauses are of length at least 2, is unsatisfiable iff at least one part is unsatisfiable.

Definition in file general.hpp.