OKlibrary  0.2.1.6
general.hpp File Reference

Investigations regarding pigeonhole clause-sets. More...

Go to the source code of this file.


Detailed Description

Investigations regarding pigeonhole clause-sets.

Todo:
Prime implicates
  • The number and the structure of prime implicates for satisfiable php is needed.
  • Simple computation via resolution closure:
    for n : 0 thru 4 do print(n, length(min_resolution_closure_cs(weak_php_cs(n,n))[1]));
    0 0
    1 1
    2 12
    3 87
    XXX
       
  • Alternative method: Expanding to canonical CNF and use Quine/McCluskey:
    # First the size of the canonical CNFs (and the total number of full clauses):
    for m : 0 thru 4 do print(m,ncl_fcs(expand_fcs(weak_php_fcs(m,m))),2^(m*m));
    0 0 1
    1 1 2
    2 14 16
    3 506 512
    4 65512 65536
    
    # Note that the number of full clauses of PHP^m_m is 2^(m*m) - m!.
    
    for m : 0 thru 4 do block([FF:standardise_fcs(expand_fcs(weak_php_fcs(m,m)))],
      output_fcs_v(
        sconcat("Canonical CNF for the pigeonhole principle (weak form) with ", m, " pigeons."),
        FF[1], sconcat("PHP_CNF_",m,".cnf"), FF[2]))$
    
    for ((n=1;n<=4;++n)); do echo ${n}; QuineMcCluskey-n16-O3-DNDEBUG PHP_CNF_${n}.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG sd nz; done
    0
         n    c     l
         0    0     0
    1
         n    c        l
         1    1        1
     length   count
          1       1
    2
         n    c        l
         4    12       24
     length   count
          2      12
    3
         n     c        l
         9    87      252
     length   count
          2      18
          3      60
          4       9
    4
          n      c        l
         16    728     3056
     length   count
          2      48
          4     488
          5     144
          6      48
       
  • We remark that PHP^m_m has exactly one DNF representation (without new variables), since the total satisfying assignments correspond 1-1 to the m! permutations of the m pigeons, and we have only these total satisfying assignments (a boolean function f has exactly one DNF representation without new variables iff f has only total satisfying assignments).
Todo:
Applying partial assignments
  • Minimally unsatisfiable sub-clause-sets of phi * weak_php_cs(m,n) for m > n:
    1. Are these all isomorphic to some weak_php_fcs(k+1,k) ?
    2. No; for example
      L3 : random_splitting_mus(weak_php_cs(7,5),3,dll_simplest_trivial2)$
      map(deficiency_cs,L3);
        [51, 47, 43, 39, 36, 32, 29, 26, 24, 20, 8, 7, 5, 3, 1, 1, 1, 1]
           
      but
      for n : 1 thru 5 do print(deficiency_weak_php(n+1,n));
      1 3 10 25 51
           
      so there are new deficiencies!
    3. Which deficiencies can be realised?
    4. What can be said about the clause-sets obtained?
    5. Perhaps deficiency 2 cannot be realised?
    6. What are the types obtained for deficiency 3 ? Experiment:
      def3cls : [];
      experiment(m,n) := block(
       [count : 0, F : weak_php_cs(m,n)],
        for seed : 0 do block(
         [L : random_splitting_mus(F,seed,dll_simplest_trivial2), S],
          print("seed:", seed, map(deficiency_cs,L)),
          S : sublist(L,lambda([F],is(deficiency_cs(F) = 3))),
          if not emptyp(S) then (
            S : map(sdp_reduction_cs, S),
            def3cls : append(def3cls,S),
            for i : 1 thru length(S) do print(count + 1, ":", S[i]),
            count : count + length(S)
          )))$
      experiment(7,5);
           
      Only php(3,2) (up to isomorphism) found for seed <= 8.
    7. To speed it out, and remove trivial cases, now with trivial DP-reduction: def3cls : []; experiment(m,n) := block( [count : 0, F : weak_php_cs(m,n)], for seed : 9 do block( [L : random_splitting_nsing_mus(F,seed,dll_simplest_trivial2), S], print("seed:", seed, map(deficiency_cs,L)), S : sublist(L,lambda([F],is(deficiency_cs(F) = 3))), if not emptyp(S) then ( def3cls : append(def3cls,S), for i : 1 thru length(S) do print(count + 1, ":", S[i]), count : count + length(S) )))$ experiment(7,5); Again, only php(3,2) (up to isomorphism) found for seed <= 20.
Todo:
MU structure
  • What about the saturation structure of PHP_n (= PHP^{n+1}_n):
    1. First just considering whether we have saturatedness:
      for n : 0 thru 4 do print(n, saturated_min_unsat_bydef_fcs(weak_php_fcs(n+1,n)));
      0 true
      1 false
      2 false
      3 false
      4 false
           
    2. The sets of partial assignments not resulting in a MU:
      # do we get all elementary partial assignments?:
      for n : 0 thru 4 do print(n, length(non_saturating_pas_bydef_fcs(weak_php_fcs(n+1,n))), 2*nvar_php(n+1,n));
      0 0 0
      1 2 4
      2 12 12
      3 12 24
      4 20 40
           
      So apparently except for n=2 we get exactly half of the elementary partial assignments; these seem to be exactly the positive assignments, except for n=1,2:
      for n : 0 thru 4 do block([F:weak_php_fcs(n+1,n)], print(n, is(non_saturating_pas_bydef_fcs(F) = singletons(F[1]))));
      0 true
      1 false
      2 false
      3 true
      4 true
      non_saturating_pas_bydef_fcs(weak_php_fcs(2,1));
        {{-php(1,1)},{-php(2,1)}}
           
    3. Clear that after setting a variable to true we get a non-MU, since if we put pigeon i into hole j, then the 2-clauses saying that pigeon pigeons k1::k2 can not go into j at the same time for i notin {k1,k2} become superfluous.
  • What about the marginality of PHP_n (= PHP^{n+1}_n):
    for n : 0 thru 4 do print(n, marginal_min_unsat_bydef_fcs(weak_php_fcs(n+1,n)));
    0 true
    1 true
    2 true
    3 true
    4 true
       
    Rather obviously all PHP_n are marginal.

Definition in file general.hpp.