OKlibrary
0.2.1.6

Investigations regarding pigeonhole clausesets. More...
Go to the source code of this file.
Investigations regarding pigeonhole clausesets.
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
# 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}; QuineMcCluskeyn16O3DNDEBUG PHP_CNF_${n}.cnf  ExtendedDimacsFullStatisticsO3DNDEBUG 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
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]
for n : 1 thru 5 do print(deficiency_weak_php(n+1,n)); 1 3 10 25 51
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);
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
# 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
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)}}
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
Definition in file general.hpp.