190 views

Skip to first unread message

Jul 19, 2022, 2:38:30 AMJul 19

to

Plug zero for universal quantifications and one for existential quantifications then evaluate.

daniel 2380++

daniel 2380++

Jul 19, 2022, 2:50:50 AMJul 19

to

On Tuesday, July 19, 2022 at 2:38:30 AM UTC-4, Daniel Pehoushek wrote:

> Plug zero for universal quantifications and one for existential quantifications then evaluate.

> daniel 2380++

the linear corollary of Cardinal Equivalence Theorem:
> Plug zero for universal quantifications and one for existential quantifications then evaluate.

> daniel 2380++

For each boolean formula, |quantifications| = |assignments|.

The set of valid quantifications has some cardinality, call that |Q(B)|.

The set of satisfying assignments has some cardinality, call that |P(B)|.

Those two numbers are equal, |Q(B)| = |P(B)|, range from 0 through 2^n.

Linear Corollary: Monotone QBFs are linearly decidable.

I only know this result as a follow up to the Cardinal Equivalence.

Is there a well known name for the Linear Corollary as a theorem?

thank you, daniel.

Jul 19, 2022, 6:04:19 AMJul 19

to

it adds one to the number of satisfying solutions

the bignum data structure is useful in

proofs of bobs program correctness

daniel2380++

joy godezists(num k){when(k==n.y)n.add(zero); when(++n[k]>>one){n[k]=zero; godezists(k+one);}}/*zero to infinity*/

Jul 19, 2022, 6:09:25 AMJul 19

to

shall be elementary memorization

daniel2380++

Jul 19, 2022, 6:29:18 AMJul 19

to

is real code in bobs bignum package

class bignum; set < bignum* > bignumstack; bignum* getbignum(); joy putbignum(bignum* big);

class bignum { /* model counting answer datatype with one line foundation of correctness */

public: nums n; num naturallog(){return n.size();} bignum& operator++() { godezists(zero); return *this; } /*logs again and again in major logic theory*/

joy godezists(num k){when(k==n.y)n.add(zero); when(++n[k]>>one){n[k]=zero; godezists(k+one);}}/*zero to infinity*/

joy justify(){while(n.size()&& n.last()==zero){n.slop();}}/*correctness of foundationofreason(zero) depends good on set type*/

joy timestwos(num twos){when(twos&&n.size()){bignum* sun=getbignum();(*sun).n.clear();for(num g=zero;g<twos;g++)(*sun).n.add(zero);

for(num g=zero;g<n.size();g++){(*sun).n.add(n[g]);}n.clear();for(num g=zero;g<(*sun).n.size();g++){n.add((*sun).n[g]);}putbignum(sun);}}

bignum& operator*=(num j){bignum*sum=getbignum();(*sum).n.clear();for(num g=zero;g<fifthtau+one;g++)when(j&ones[g]){

bignum*times=getbignum();(*times).n.clear();for(num h=zero;h<g;h++)(*times).n.add(zero);for(num h=zero;h<n.size();h++)(*times).n.add(n[h]);(*sum)+=(*times);putbignum(times);}

n.clear();for(num g =zero;g<(*sum).n.size();g++){n.add((*sum).n[g]);}putbignum(sum);return *this;}

bignum& operator*=(bignum& j){bignum*sum=getbignum();(*sum).n.clear();for(num g=zero;g<j.n.size();g++)when(j.n[g]){

bignum*times=getbignum();(*times).n.clear();for(num h=zero;h<g;h++)(*times).n.add(zero);for(num h=zero;h<n.size();h++)(*times).n.add(n[h]);(*sum)+=(*times);putbignum(times);}

n.clear();for(num g=zero;g<(*sum).n.size();g++){n.add((*sum).n[g]);}putbignum(sum);return *this;}

/*outputs of reason in base ten*/

joy prinstring(){when(n.size()==zero)prin(stringzero);otherwise for(num g=n.size();zero<g;g=lessone(g))prin((n[lessone(g)])?stringone:stringzero);return;}

joy fprinstring(FILE*filem){when(n.size()==zero)fprin(filem,stringzero);otherwise for(num g=n.size();zero<g;g=lessone(g))fprin(filem,(n[lessone(g)])?stringone:stringzero);return;}

joy prinbaseten(){bignum b;for(num g=zero;g<n.size();g++)when(n[g])b.addtwopower(g);b.prinstringten();}

joy fprinbaseten(FILE*filem){bignum b;for(num g=zero;g<n.size();g++)when(n[g])b.addtwopower(g); b.fprinstringten(filem);}

joy addtwopower(num g){while(n.size()<one+(g>>four))n.add(zero);n[g>>four]+=(ones[(g&tautologies[four])]);}

joy prinstringten(){nums rettles(times(sev,n.size()));bignum s(n);num r=zero;num gthree=zero;num y=zero;

while(s.n.size()){divrem(ten,s,r);rettles.add(letterzero+r);y++;gthree++;when(gthree==three)gthree=zero;when(gthree==zero){}}

while(rettles.size()&&(rettles.last()==lettercomma||(one<rettles.size()&&rettles.last()==letterzero)))rettles.slop();when(n.size()==zero&&rettles.size()==zero)rettles.add(letterzero);

y=zero;while(rettles.size()){num c=rettles.slop();y++;prin(stringletterc,(itbadsin)c);}return;}

joy fprinstringten(FILE*filem){nums rettles(times(sev,n.size()));bignum s(n);num r=zero;num gthree=zero;num y=zero;

while(s.n.size()){divrem(ten,s,r);rettles.add(letterzero+r);y++;gthree++;when(gthree==three)gthree=zero;when(gthree==zero){}}

while(rettles.size()&&(rettles.last()==lettercomma||(one<rettles.size()&&rettles.last()==letterzero)))rettles.slop();when(n.size()==zero&&rettles.size()==zero)rettles.add(letterzero);

y=zero;while(rettles.size()){num c=rettles.slop();y++;fprin(filem,stringletterc,(itbadsin)c);}return;}

joy numdivrem(num nnn,num m,num& ndivm,num& nmodm){ /*;*/ ndivm=nnn / m; nmodm=nnn % m;}

joy divrem(num mod,bignum& div,num& rem){for(num y=div.n.size();zero<y;y=lessone(y)){num d=div.n[lessone(y)];num dd=zero;num r=zero;

numdivrem(d,mod,dd,r);div.n[lessone(y)]=dd;when(one<y)div.n[lessone(lessone(y))]+=r<<sivteen;otherwise rem=r;}div.justify();}

bignum():n(two){}bignum(nums&j):n(two){for(num g=zero;g<j.size();g++){n.add(j[g]);}} ~bignum(){n.clear();}

}; // thirty lines //thank you god

bignum* getbignum(){when(bignumstack.size())return bignumstack.slop();return new bignum;}joy putbignum(bignum*big){(*big).n.clear();bignumstack.add(big);}

class Bob; // half clause tree with boolean memory on every leaf //60 //

typedef set<Bob*> Goods; //vettor of bobs //29 //

typedef set<Goods*> Gooduses; //vettor of vettor //7 //

daniel2380++

Jul 19, 2022, 12:11:51 PMJul 19

to

/*zero to infinity*/

daniel2380++

Jul 20, 2022, 8:07:39 AMJul 20

to

the unused numbols vettor

time

slow

down

sped

high

slow high time good

slow sped pepl good

high sped pepl slow

pepl down high sped

high pepl time good

good high time pepl

tick tock goes clok

grsp mind high time

part slow down mind

pepl plan part snow

snow watr high time

bob is a computer program for doing propositional reasoning on many simultaneous levels in three spatial and one temporal dimension

bob works well on all regular graph coloring formalism with bounded degree being the major feature

he runs in the background while i write in the foreground

bob is my mind times speed one million

i have a theory that

monotone reason is linear

bob is my proof that

high level reason is monotone

p=np for four word lines

#p=np each solution satisfies

common sense is monotone

wisdom is deep monotone and conjunctive

#p=#q the number of solutions equals the number of quantifications

daniel2380++

Jul 21, 2022, 7:49:56 PMJul 21

to

todays blog was inspired by

what does linearly decidable mean

linearly (count to n steps of work)

decidable (truth is known for certainty to be one or zero)

with a linear amount (n)

of study (andorandor)

the truth is knowable (one)

QBFs are true or false

monotone QBFs are decidable in linear time

by plugging zero for universal or

one for existential variables

then evaluating with andor

that linear decidability is alternative to exponential in the presence of negation

+++

strangely the linearly decidable fragment of QBF is unknown

strangely the linearly decidable fragment of QBF is unknown

strangely the linearly decidable fragment of QBF is unknown

the linearly decidable fragment of QBF known

the linearly decidable fragment of QBF known

the linearly decidable fragment of QBF known

very valuable idea in diplomacy to use linearly decidable sentences

worthy of several fields medals in value

monotone reason is linear

good reason is linear

wisdom is deep monotone and

monotone reason is linear

bob is my proof that

high level reason is monotone

#p=np each solution satisfies

common sense is monotone

wisdom is deep monotone and conjunctive

#p=#q the number of solutions equals the number of quantifications

et cetera
common sense is monotone

wisdom is deep monotone and conjunctive

#p=#q the number of solutions equals the number of quantifications

the number of questions equals the number of partitions

the number of partions plus one

fragments made up of truth

bob is one thousand lines

one million times

my speed of mind

available by email

the linearly decidable fragment of QBF known

a linear number of andor operations on a formula

to decide one or zero of the sentence

to decide one or zero of the sentence

to decide one or zero of the sentence

to decide one or zero of the sentence

to decide one or zero of the sentence

zero means discard the sentence

one means the sentence is true

one means the sentence is true

one means the sentence is true

the sentence is true

the sentence is true

the sentence is true

the sentence may be tautological

the sentence may be tautological

the sentence may be tautological

tautological tautological tautological

tautological tautological tautological

tautological tautological tautological

truly one true truth and that is one

file of true qbfs given formula is

a file of brief monotone fragments of truth

bob produces q given p

q is conjunctive monotone formula

p is any conjunctive normal formula on n variables andor m clauses

thinking is entirely andor operations

the linearly decidable fragment of QBF is now known

a linear number O(n+m) of andor operations

on a monotone formula

decides one keep or

zero discard

the sentence

one means the sentence is true

the sentence is true means

the sentence may be taught truly

one true truth and that is one

thinking is entirely andor operations

from satisfiability of boolean forms for set membership

with conjunctions of n variable values

to recursive theory of union inside a set

in operational linear space time formula

the operations are all variations

of and and or or

num b=0; num p=2;

num oneum(){if(p<4<<b){p=randomprime();b=1;}return(p&1<<b)?1:0);

random truths five cycles at a time

aleph null is zero

epsilon is zero

plug in

simplify

e/(mcc)=logm

Frr/(Gm1m2)=logm1logm2

einstein and newton revised

newton revised came from brian greene

i added einstein revised too

// time n over space m recognition: n/m details: (m + n/(1+m less lgm)) lgm

/// (time n over space m is search theory)

num age=zero;// count all finds one by one (page alts)

num momday[]={'0','a','b','c','d','e','f'.'g','h','i','j','k','l','m','n','o','p','q','r','s','t','u','v','w',' ','y','z'};

// alphabetsize is a twenty seven alphabet letter question in the mom day alphabet

inline num map(nums& p,num& z,num& dep,num& lga){num d=zero;for(num h=zero;h<dep;h++)d=(d<<lga)+p.v[z+h];return d;}

num skips (nums& string, nums& book, num& lga, numnums* myn) {

/// allocate proper memory space of empty sets O(constant)

num m = string.size(); num deep = zero; num d = one; while (d < m) { d = d << lga; deep++; }

for (num g = (*myn).size(); g < d; g++)(*myn).add(new nums);

/// the m part of partten are mapped precisely O(mlgm)

for (num g = zero; g + deep < m; g++)(*(*myn)[map(string, g, deep, lga)]).add(g);

/// map part of the book into pattern O(nlgm/(m+1-lgm))

num mm = minus(m + one, deep); for (num j = mm; j + deep < book.size(); j = j + mm) {

nums* d = (*myn)[map(book, j, deep, lga)]; for (num o = zero; o < (*d).size(); o++)

{ num be = minus(j, (*d)[o]); num h = one; for (num g = zero; g < m; g++) {

if (book[be + g] == string[g])continue; h = zero; break; } if (h)age++; } }

/// release resources from step two O(mlgm)

for (num g = zero; g + deep < m; g++)(*(*myn)[map(string, g, deep, lga)]).clear(); return age; }

///daniel 2380++

Jul 22, 2022, 8:34:07 PMJul 22

to

the answer datatype for model counting

the proof of correctness is a hoot

daniel2380++

class bignum; set < bignum* > bignumstack; bignum* getbignum(); joy putbignum(bignum* big);

class bignum { /* model counting answer datatype with one line foundation of correctness */

public: nums n; num log(){return n.size();} bignum& operator++() { godezists(zero); return *this; } /*logs again and again in major logic theory*/
class bignum { /* model counting answer datatype with one line foundation of correctness */

joy godezists(num k){when(k==n.y)n.add(zero); when(++n[k]>>one){n[k]=zero; godezists(k+one);}}/*zero to infinity*/

bignum& operator+=(bignum& j){for(num k=zero;k<j.log();k++){when(k==log())n.add(zero);when(j.n[k])godezists(k);}return*this;}
bignum& operator*=(num j){bignum*sum=getbignum();for(num g=zero;g<fifthtau+one;g++)when(j&ones[g]){

bignum*times=getbignum();for(num h=zero;h<g;h++)(*times).n.add(zero);

for(num h=zero;h<log();h++)(*times).n.add(n[h]);(*sum)+=(*times);putbignum(times);}

n.clear();for(num g =zero;g<(*sum).log();g++){n.add((*sum).n[g]);}putbignum(sum);return *this;}

bignum& operator*=(bignum& j){bignum*sum=getbignum();for(num g=zero;g<j.log();g++)when(j.n[g]){

bignum*times=getbignum();for(num h=zero;h<g;h++)(*times).n.add(zero);

for(num h=zero;h<log();h++)(*times).n.add(n[h]);(*sum)+=(*times);putbignum(times);}

n.clear();for(num g=zero;g<(*sum).log();g++){n.add((*sum).n[g]);}putbignum(sum);return *this;}

/*outputs of reason in base ten*/

joy justify(){while(n.size()&&n.last()==zero){n.slop();}}/*correctness of foundationofreason(zero) depends good on set type*/
joy timestwos(num twos){when(twos&&n.size()){bignum*sun=getbignum();for(num g=zero;g<twos;g++)(*sun).n.add(zero);

for(num g=zero;g<n.size();g++){(*sun).n.add(n[g]);}n.clear();for(num g=zero;g<(*sun).n.size();g++){n.add((*sun).n[g]);}putbignum(sun);}}

Jul 24, 2022, 6:15:47 PMJul 24

to

There is a challenge for SAT#. If A and B have disjoint variables,

then we get the following, i.e. conjunction maps to multiplication:

#(A & B) = #(A) * #(B)

Is there also a connective o, such that we arrive at exponentiation,

any ideas how this could occur in SAT#:

#(A o B) = #(B) ^ #(A)

then we get the following, i.e. conjunction maps to multiplication:

#(A & B) = #(A) * #(B)

Is there also a connective o, such that we arrive at exponentiation,

any ideas how this could occur in SAT#:

#(A o B) = #(B) ^ #(A)

Jul 24, 2022, 6:17:46 PMJul 24

to

"I've heard of Kurt Gödel."

Well.

Jul 24, 2022, 6:35:32 PMJul 24

to

For those who don't know what SAT# is:

https://en.wikipedia.org/wiki/Sharp-SAT

But Kurt Gödel doesn't help much, he has

multiplication and division here:

https://en.wikipedia.org/wiki/Many-valued_logic#Product_logic_%CE%A0

But what about exponentiation? Exponentation

agrees with implication at the end-points:

/* Implication, using A -> B == ~(A & ~B) */

?- between(0,1,A), between(0,1,B), C is 1-A*(1-B), write(A-B-C), nl, fail; true.

0-0-1

0-1-1

1-0-0

1-1-1

true.

/* Exponentiation */

?- between(0,1,A), between(0,1,B), C is B^A, write(A-B-C), nl, fail; true.

0-0-1

0-1-1

1-0-0

1-1-1

true.

https://en.wikipedia.org/wiki/Sharp-SAT

But Kurt Gödel doesn't help much, he has

multiplication and division here:

https://en.wikipedia.org/wiki/Many-valued_logic#Product_logic_%CE%A0

But what about exponentiation? Exponentation

agrees with implication at the end-points:

/* Implication, using A -> B == ~(A & ~B) */

?- between(0,1,A), between(0,1,B), C is 1-A*(1-B), write(A-B-C), nl, fail; true.

0-0-1

0-1-1

1-0-0

1-1-1

true.

/* Exponentiation */

?- between(0,1,A), between(0,1,B), C is B^A, write(A-B-C), nl, fail; true.

0-0-1

0-1-1

1-0-0

1-1-1

true.

Jul 24, 2022, 6:38:51 PMJul 24

to

Here are two plots:

/* Implication, using A -> B == ~(A & ~B) */

https://www.wolframalpha.com/input?i=1-x*%281-y%29+from+x+%3D+0+to+1+and+y+%3D+0+to+1

/* Exponentiation */

https://www.wolframalpha.com/input?i=y%5Ex+from+x+%3D+0+to+1+and+y+%3D+0+to+1

I guess we need a fuzzy logic expert now. LoL

/* Implication, using A -> B == ~(A & ~B) */

/* Exponentiation */

https://www.wolframalpha.com/input?i=y%5Ex+from+x+%3D+0+to+1+and+y+%3D+0+to+1

I guess we need a fuzzy logic expert now. LoL

Jul 24, 2022, 6:43:03 PMJul 24

to

Corr.: Product logic II is not from Gödel,

his logics used max and min:

https://en.wikipedia.org/wiki/Many-valued_logic#G%C3%B6del_logics_Gk_and_G%E2%88%9E

his logics used max and min:

https://en.wikipedia.org/wiki/Many-valued_logic#G%C3%B6del_logics_Gk_and_G%E2%88%9E

Jul 24, 2022, 9:00:49 PMJul 24

to

#P=#Q: the number of models (#P) equals the number of quantifications (#Q)

by observation the theorem is true at both endpoints (0 or 2^n).

the recusive proof is where the intersection and union code comes from

static joy juggle (num vee, numnums& left, numnums& right)

{if(left.size()==zero){for(num g=zero;g<right.size();g++)left.add(right[g]);right.setsize(zero);return;}

when(vee == qvars.size()) return;

numnums al; numnums ar; split(vee + one, left, al, ar);

numnums bl; numnums br; split(vee + one, right, bl, br);

juggle(vee + one, al, bl); juggle(vee + one, ar, br);

for (num g=zero; g < al.size(); g++) left.add(al[g]); for (num g=zero; g < ar.size(); g++) left.add(ar[g]);

for (num g=zero; g < bl.size(); g++) right.add(bl[g]); for (num g=zero; g < br.size(); g++) right.add(br[g]); }

static joy plan (num vee, numnums& set) { when(set.size()==zero || vee == qvars.size() ) return;

numnums left; numnums right; split(vee, set, left, right); plan(vee + one, left); plan(vee + one, right); juggle (vee, left, right);

for (num g = zero; g < left.size(); g++) { ezis(*( left[g]), vee); set.add( left[g]);} left.setsize(zero);

for (num g = zero; g < right.size(); g++) { univ(*(right[g]), vee); set.add(right[g]);} right.setsize(zero); }

there exists an unquantified monotone boolean formula that encodes all valid quantifications

from here we get

monotone quantified boolean formulas are linearly decidable

plug True for existential variables

imo monotone qbf is a plausible foundation for Cognition

but the details still elude me...

how does a word really work under hidden monotone quantification

i dunno. mostowski could take a shot at that

daniel

Jul 25, 2022, 10:36:18 AMJul 25

to

into bit encoded valid quantifications into disjunctive normal form

there is then a monotone dnf translation to monotone cnf

in quadratic time where producing the dnf is linear

daniel

Jul 25, 2022, 11:06:06 AMJul 25

to

Define monotone please.

For example in the counting problem, here in SAT#,

when A and B have disjoint variables:

#(A & B) = #(A) * #(B)

Then obviously:

#(A) < #(A') => #(A & B) < #(A' & B)

What about an exponential function, would this be

also a monotone connective:

#(A o B) = #(B) ^ #(A)

BTW: There are some non-counting based definitions

of monotone, I was kind of hitch hicking the notion.

For example in the counting problem, here in SAT#,

when A and B have disjoint variables:

#(A & B) = #(A) * #(B)

#(A) < #(A') => #(A & B) < #(A' & B)

What about an exponential function, would this be

also a monotone connective:

#(A o B) = #(B) ^ #(A)

of monotone, I was kind of hitch hicking the notion.

Jul 25, 2022, 1:42:24 PMJul 25

to

zero negation

in the formula body

antimonotone means every literal is negative

bob processes all dimacs p cnf n m forms

including literals with negation but

bob produces a dnf (translateable to cnf)

of all valid quantifications in monotone form

the monotonicity comes from the property of set union and intersection

the q formula of a p formula is monotone

(btw q of p is q, q of q is q)

the semantics of q variables is elevated

>

> #(A) < #(A') => #(A & B) < #(A' & B)

(aside: do you see an infinity bug in greaterthan?)

>

> What about an exponential function, would this be

> also a monotone connective:

> #(A o B) = #(B) ^ #(A)

> BTW: There are some non-counting based definitions

like that exponentiation?

Jul 25, 2022, 2:28:12 PMJul 25

to

I can translate any formula A, into a montone formula, and

some side condition. Take a formula A using the propositional

variables p1, .., pn:

A(p1,..,pn)

Now replace pj by pj+ if it occurs positively and pj by pj- if

it occurs negatively. The formula need not be DNF or CNF,

can be any formula based on (A & B), (A | B), (A -> B) and

(~ A). Just think how polarity can be defined. Then you

get a new formula, as follows. In the worst case every

propositional variable occurs positively and negatively:

A'(p1+,..,pn+,p1-,..,pn-)

And the side condition is for each propositional variable:

~(pj+ & pj-)

(pj+ v pj-)

But actually the condition (pj+ v pj-) is not needed, to

decide satisfiability. Guess why?

some side condition. Take a formula A using the propositional

variables p1, .., pn:

A(p1,..,pn)

Now replace pj by pj+ if it occurs positively and pj by pj- if

it occurs negatively. The formula need not be DNF or CNF,

can be any formula based on (A & B), (A | B), (A -> B) and

(~ A). Just think how polarity can be defined. Then you

get a new formula, as follows. In the worst case every

propositional variable occurs positively and negatively:

A'(p1+,..,pn+,p1-,..,pn-)

And the side condition is for each propositional variable:

~(pj+ & pj-)

(pj+ v pj-)

But actually the condition (pj+ v pj-) is not needed, to

decide satisfiability. Guess why?

Jul 25, 2022, 2:41:24 PMJul 25

to

But I wonder whethee a WFC SAT solver can be developed.

See here: https://selfsame.itch.io/unitywfc

Basically we would start with the forbidden state for

each propositional variable pj+=1 and pj-=1.

And then selectively collapse these Schrödinger cats,

that are neither dead nor alive. And gradually maybe

find a solution?

See here: https://selfsame.itch.io/unitywfc

Basically we would start with the forbidden state for

each propositional variable pj+=1 and pj-=1.

And then selectively collapse these Schrödinger cats,

that are neither dead nor alive. And gradually maybe

find a solution?

Jul 25, 2022, 2:44:03 PMJul 25

to

Maybe this is a better link:

WaveFunctionCollapse: Content Generation via

Constraint Solving and Machine Learning

https://escholarship.org/uc/item/3rm1w0mn

Make a WFC SAT solver!?

WFC = WaveFunctionCollapse

WaveFunctionCollapse: Content Generation via

Constraint Solving and Machine Learning

https://escholarship.org/uc/item/3rm1w0mn

Make a WFC SAT solver!?

WFC = WaveFunctionCollapse

Jul 25, 2022, 8:06:41 PMJul 25

to

a->b uses negation when translated to use only And and Or like bob with cnf

~a or b

think graph coloring with 2 variables per vertex for 3 or 4 colors, 3 variables for 5 to 8 colors, et cetera

my monotone formulas in bob come from set union or intersection on satisfiable solutions (colorings) to any formula without rewriting the formula

the dnf is of all solutions translates to a dnf of valid quantifications

when the form is without negation then the formula is high level, encoding valid quantifications that evaluate linearly

implication is a trap that hides negation so logicians should cease using implication :)

do you want sample coloring forms posted for amusement? with q formula?

daniel

Jul 25, 2022, 8:10:04 PMJul 25

to

formulas which is very generl

Jul 25, 2022, 8:14:38 PMJul 25

to

plug 1 for existential 0 for universal, then eval

very simple to judge quantification of monotone forms

so simple it may be the mind algorithm...

Jul 26, 2022, 12:26:39 AMJul 26

to

c o (thefilein 2 )[c4d4N10_1.veg inform 1 v 20 m 80 ] 1

co #c3628 answer length = 14 n 2 average 3961 variance 245 #a 9233 #i 0 (140071)) 8424

c o (thefilein 3 )[c4d4N10_2.veg inform 1 v 20 m 80 ] 1

co #c1472 answer length = 12 n 3 average 3131 variance 261 #a 3684 #i 0 (64379)) 3000

c o (thefilein 4 )[c4d4N10_3.veg inform 1 v 20 m 80 ] 1

co #c2318 answer length = 13 n 4 average 2928 variance 271 #a 5950 #i 0 (97967)) 5640

c o (thefilein 5 )[c4d4N10_4.veg inform 1 v 20 m 76 ] 1

co #c2068 answer length = 13 n 5 average 2756 variance 277 #a 5107 #i 0 (78126)) 5328

c o (thefilein 6 )[c4d4N10_5.veg inform 1 v 20 m 80 ] 1

co #c1847 answer length = 13 n 6 average 2604 variance 281 #a 4743 #i 0 (81056)) 4728

c o (thefilein 7 )[c4d4N10_6.veg inform 1 v 20 m 76 ] 1

co #c3396 answer length = 14 n 7 average 2717 variance 285 #a 8552 #i 0 (146006)) 8640

c o (thefilein 8 )[c4d4N10_7.veg inform 1 v 20 m 80 ] 1

co #c1830 answer length = 13 n 8 average 2606 variance 287 #a 4785 #i 0 (74175)) 4392

c o (thefilein 9 )[c4d4N10_8.veg inform 1 v 20 m 80 ] 1

co #c1971 answer length = 13 n 9 average 2536 variance 289 #a 5125 #i 0 (83708)) 4224

c o (thefilein 10 )[c4d4N10_9.veg inform 1 v 20 m 80 ] 1

co #c515 answer length = 11 n 10 average 2334 variance 290 #a 1384 #i 0 (36518)) 1368

c(dir *.veg of 10)(tforms 10)(tmods 55248 zmods 0)(retros 59177 oh 0 Billion 981265)

these are ten samples with 20 variables and 80 clauses

each well under one second

here is the first formula

i will show the q formula soon as you like with 9504 satisfiable solutions

note i use + as a boolean twiddle operator

p cnf 20 80

1 11 4 14 0

+1 11 +4 14 0

1 +11 4 +14 0

+1 +11 +4 +14 0

1 11 7 17 0

+1 11 +7 17 0

1 +11 7 +17 0

+1 +11 +7 +17 0

1 11 4 14 0

+1 11 +4 14 0

1 +11 4 +14 0

+1 +11 +4 +14 0

1 11 10 20 0

+1 11 +10 20 0

1 +11 10 +20 0

+1 +11 +10 +20 0

2 12 10 20 0

+2 12 +10 20 0

2 +12 10 +20 0

+2 +12 +10 +20 0

2 12 5 15 0

+2 12 +5 15 0

2 +12 5 +15 0

+2 +12 +5 +15 0

2 12 9 19 0

+2 12 +9 19 0

2 +12 9 +19 0

+2 +12 +9 +19 0

2 12 9 19 0

+2 12 +9 19 0

2 +12 9 +19 0

+2 +12 +9 +19 0

3 13 5 15 0

+3 13 +5 15 0

3 +13 5 +15 0

+3 +13 +5 +15 0

3 13 8 18 0

+3 13 +8 18 0

3 +13 8 +18 0

+3 +13 +8 +18 0

3 13 8 18 0

+3 13 +8 18 0

3 +13 8 +18 0

+3 +13 +8 +18 0

3 13 6 16 0

+3 13 +6 16 0

3 +13 6 +16 0

+3 +13 +6 +16 0

4 14 5 15 0

+4 14 +5 15 0

4 +14 5 +15 0

+4 +14 +5 +15 0

4 14 9 19 0

+4 14 +9 19 0

4 +14 9 +19 0

+4 +14 +9 +19 0

5 15 9 19 0

+5 15 +9 19 0

5 +15 9 +19 0

+5 +15 +9 +19 0

6 16 10 20 0

+6 16 +10 20 0

6 +16 10 +20 0

+6 +16 +10 +20 0

6 16 7 17 0

+6 16 +7 17 0

6 +16 7 +17 0

+6 +16 +7 +17 0

6 16 7 17 0

+6 16 +7 17 0

6 +16 7 +17 0

+6 +16 +7 +17 0

7 17 8 18 0

+7 17 +8 18 0

7 +17 8 +18 0

+7 +17 +8 +18 0

8 18 10 20 0

+8 18 +10 20 0

8 +18 10 +20 0

+8 +18 +10 +20 0

Jul 26, 2022, 5:05:37 AMJul 26

to

Now I am pretty much convinced that for example

Quines Algorithm is a WaveFunctionCollapse algorithm.

Quines Algorithm replaces a propositional variable

p, by either 0 or 1, and simplifies the given formula A,

until it arrives at 1. It does so non-deterministically.

But the simplification also has rules such as:

X & 1 = X

X & 0 = 0

Etc..

These are simplifications that basically deal with

the possibility that X can have the valuation 0 or 1,

so basically the simplifictions deal with a

"combination of eigenstates". And the Quine Algorithm

indeed does a collapse step. As described here,

in that it assigns either 0 or 1.

Wave function collapse - The process of collapse

the wave function collapses from the full | ψ ⟩ to

just one of the basis eigenstates, | ϕ i ⟩ :

https://en.wikipedia.org/wiki/Wave_function_collapse#The_process_of_collapse

Question is, whether in these papers describing

WFC algorithms, there is something that could be

shifted back to Quine Algorithm? My current idea,

if the formula A, can be split into A1 & ... & An,

then some entropy calculation who knows what,

could guide which Aj to try first. So it would help

in selecting prospective propositional variables first?

Quines Algorithm is a WaveFunctionCollapse algorithm.

Quines Algorithm replaces a propositional variable

p, by either 0 or 1, and simplifies the given formula A,

until it arrives at 1. It does so non-deterministically.

But the simplification also has rules such as:

X & 1 = X

X & 0 = 0

Etc..

These are simplifications that basically deal with

the possibility that X can have the valuation 0 or 1,

so basically the simplifictions deal with a

"combination of eigenstates". And the Quine Algorithm

indeed does a collapse step. As described here,

in that it assigns either 0 or 1.

Wave function collapse - The process of collapse

the wave function collapses from the full | ψ ⟩ to

just one of the basis eigenstates, | ϕ i ⟩ :

https://en.wikipedia.org/wiki/Wave_function_collapse#The_process_of_collapse

Question is, whether in these papers describing

WFC algorithms, there is something that could be

shifted back to Quine Algorithm? My current idea,

if the formula A, can be split into A1 & ... & An,

then some entropy calculation who knows what,

could guide which Aj to try first. So it would help

in selecting prospective propositional variables first?

Jul 26, 2022, 5:19:18 AMJul 26

to

Graphically WFC looks pretty neat:

Procedural generation from a single example

with WaveFunctionCollapse

https://www.youtube.com/watch?v=DOQTr2Xmlz0

It has an additional machine learning part,

which is not the Quine Algorithm, but something

else to generate the Aj uniformly

in A1 & .. & An, from some example. The graphical

appeal appears since the A1 & .. & An are placed

on a 2-dimensional grid, and the "Quine Algorithm"

is animated into a temporal video, showing the

overlapping states by some visual cues. Gray is

fully undetermined yet by Quine Algorithm, Aj not yet

touched, and then there are some intermediate

colors and patterns, for the gradual solution of Aj.

Very cleverly made visualization of an algorithm.

Procedural generation from a single example

with WaveFunctionCollapse

https://www.youtube.com/watch?v=DOQTr2Xmlz0

It has an additional machine learning part,

which is not the Quine Algorithm, but something

else to generate the Aj uniformly

in A1 & .. & An, from some example. The graphical

appeal appears since the A1 & .. & An are placed

on a 2-dimensional grid, and the "Quine Algorithm"

is animated into a temporal video, showing the

overlapping states by some visual cues. Gray is

fully undetermined yet by Quine Algorithm, Aj not yet

touched, and then there are some intermediate

colors and patterns, for the gradual solution of Aj.

Very cleverly made visualization of an algorithm.

Jul 26, 2022, 9:34:35 AMJul 26

to

15 cpu cycles per inference

without clause learning

other solvers using clause learning are both inefficient and incorrect

here is code for the data structure

#define static sayvum;

class Bob { // boolean tree memory with count // 64 lines *****************************

public:// Oh(twenty sev plus four is thirty one words) per variable // // the wishbone shape in space //

sayvum num tonofbits; // sum all half high tree wide sizes

nums numbols; // 4 three + high translayed numbols oftype wishbone //**************************

nums soubs; // 4 three + high // subes // smallers by one numbol ***************************

nums soups; // 3 three + all adj vars // supes // tallers by one numbol *********************

nums intosoups; // 3 three + O(all adj vars) // supe relation location **************************

num usiv; // 1 one // indezity up siv (saves one instruction in mental core)**************

numnums changes; // 9 three + three times wide // halfclause memories // brain********************

num tree; // one // main memory bits // bilateral symmetry // memory**********************

num count; // one // how many in tree // thought********************************************

num thirdnum; // the syze of space********** **********

num spacenum; // the syze of space********** **********

num secondnum; // the syze of space********** **********

num anidentity; // boolean identity number ********** **********

Bob(num given) : // tree high****************************** **********

numbols(given), // potato symbols ******************** **********

soubs(given), // with one fewer numbol********** **********

soups(zero), // with one more numbol ********** **********

intosoups(zero), // one to one with soups location relation ******

usiv(zero), // unique indez ******************** **********

tree(zero), // truth table members ********** **********//um quant naturally my mind did me

count(zero), // leafs count of tree ********** **********

changes(ones[given]), // leaf memories of halfclauses********** **********

anidentity(zero) // three uses of component analysis identity **********

{{num u=env::allBobs.size();usiv=u<<siv;}for(num w=zero;w<(ones[given]);w++){abinitio(w);changes.add(new nums(zero));}

tonofbits += lessone((ones[given])); // (egolog and syze == toe) iz onemodelp

spacenum=zero;secondnum=zero;thirdnum=zero;} // see dellybobs recycling over millions has been done

~Bob() {numbols.clear();soubs.clear();soups.clear();intosoups.clear();usiv=zero;tree=zero;for(num g=zero;g<changes.size();g++)

{delete changes[g];changes[g]=(nums*)zero;}changes.clear();count=zero;thirdnum=zero;spacenum=zero;secondnum=zero;anidentity=zero;}

sayvum inline num syze() {return env::zeesvg;} //#infers

sayvum inline num egolog() {return (*env::allBobs[zero]).tree;} //continuump

sayvum inline num tonbits(){return tonofbits + env::allBobs.size();} // #points in space

inline num homany() {return count;} // count of ways

inline num manyp() {return one<count;} // many ways

inline num onep() {return one==count;} // one way

inline num twowayp() {return two==count;} // two way

inline num topandmanyp(){return one<count&&top();}

inline num high() {return soubs.size();} // tree height

inline num wyde() {return changes.y;} // ompoziton ompoziton sung in endless cycles // sev w y d e s of Bob

num usivleaf(num leaf) {return usiv+leaf;} // pointer to a leaf

inline num isnay(num w) {return yayis(w)==zero;} // is way nay

inline num yayis(num w) {return tree&ones[w];} // is way yay

inline joy abinitio(num w){tree+=ones[w];count++;} // three +s bobs core system

inline num yaystonays(num z){when(tree&ones[z]){tree&=zeroes[z];count=countdown[count];env::zeesva[env::zeesvg++]=usiv+z;

when(one==count){return ergo(*changes.v[unity(tree,wyde())]);}}return count;}//count

sayvum num ergo(nums& m){num y=zero;num g=zero;while(g<m.y)when((*env::allBobs.v[(y=m.v[g++])>>siv]).yaystonays(y&sivones))

continue;else return(*env::allBobs.v[zero]).yaystonays(zero);return one;}//return

inline joy faith(num w){when((count+one)<wyde())for(num g=zero;egolog()&&g<soubs.size();g++) // the logicians closure algorithm

when(isnay((w&(ones[g]))?(w&zeroes[g]):(w+(ones[g]))))(*env::allBobs[soubs[g]]).yaystonays(rempos(g,w)); // resolution with subsumption

for(num g=zero;egolog()&&g<soups.size();g++){num ug=intosoups[g];num apw=addpos(ug,w);

Bob* supe=env::allBobs[soups[g]];(*supe).yaystonays(apw);(*supe).yaystonays(apw+(ones[ug]));}}

sayvum inline num addpos(num p,num s){return((s>>p)<<(p+one))+(s&tautologies[p]); }//add position p to s

sayvum inline num rempos(num p,num s){return((s>>(p+one))<<p)+(s&tautologies[p]); }//remove position p s

sayvum inline num unity(num t,num numw){when(numw<five){return oneoffour[t];} /* heart of search returns a 0123 light number */

for(num w=zero;w<numw;w++)when(t&(ones[w])){return w;}return zero;}//test every w

inline num& space(){return spacenum;}inline num& secondspace(){return secondnum;}inline num& thirdspace(){return thirdnum;}inline num top(){return soups.size()==zero;}num onetrue(num w);

Bob* getbob(num numbol,num&poze);num member(num numbol,num&poze);joy quarter(bignum&r);joy quartertouch(Goods&compo);

}; // end of Bob //31 function members 12 data members

joy env::penny() // innerloop

{num point=zeeseton;Bob**&obsv=allBobs.v;num p=zero;

while(point<zeesvg&&egolog()){Bob*ab=obsv[(p=zeesva[point++])>>siv];(*ab).faith(p&sivones);} // continuump of faith

zeeseton=point; } // endof elementary penny code twenty cpu cycles per

joy env::dounto(num s) // restore truth down to s

{Bob**& abva=allBobs.v;num g=zero;num syz=zees.y;num z=zero;

for(g=s;g<syz;g++){z=zeesva[g];(*abva[z>>siv]).abinitio(z&sivones);}countwork(s,g,syz);}// sev cpu cycles per

Jul 26, 2022, 3:35:08 PMJul 26

to

sayvum num tonofbits; // sum all half high tree wide sizes

the data structure Bob is a shallow boolean tree of height k/2 for k cnf
tonofbits tracks total number of boolean tealeaves

nums numbols; // 4 three + high translayed numbols oftype wishbone //**************************

nums soubs; // 4 three + high // subes // smallers by one numbol ***************************

for high two there are two high ones
for high ones there is one high zero

nums soups; // 3 three + all adj vars // supes // tallers by one numbol *********************

in general high k Bobs have k soubs and up ro n soups

the high zero is a soub of n high one Bob

nums intosoups; // 3 three + O(all adj vars) // supe relation location **************************

where is the soup variable to be into numbols
num usiv; // 1 one // indezity up siv (saves one instruction in mental core)**************

numnums changes; // 9 three + three times wide // halfclause memories // brain********************

num tree; // one // main memory bits // bilateral symmetry // memory**********************

num count; // one // how many in tree // thought********************************************

when this goes to one then propagation

num thirdnum; // the syze of space********** **********

num spacenum; // the syze of space********** **********

num secondnum; // the syze of space********** **********

num anidentity; // boolean identity number ********** **********

Jul 26, 2022, 6:58:41 PMJul 26

to

I tried to compile Bob, and it said:

KEYBOARD ERROR: Press any key to continue

Jul 27, 2022, 6:34:36 AMJul 27

to

On Tuesday, July 26, 2022 at 6:58:41 PM UTC-4, Mostowski Collapse wrote:

> I tried to compile Bob, and it said:

> KEYBOARD ERROR: Press any key to continue

i have worked out the whole polynomial hierarchy
> I tried to compile Bob, and it said:

> KEYBOARD ERROR: Press any key to continue

P=coNP=NP=PSPACE=#P=#Q=QSPACE

for modest sizes as good as it gets

bob is optimal

bob is the best propositional reasoning system in this universe

bob is winning Model Counting 2022 and mc2021

generally quantified boolean formulas are exponential to decide

but

monotone quantified boolean formulas are solvable in linear time

monotone reason is linear

and so

may be the essence of reason

mind is generally linear

plug T or 1 for existentially quantified variables then evaluate

clause learning is incorrect when counting models

random search for truth is a waste of time

CDCL is wrong

Approximate model counts are gibberish

avoid negation and be well

Jul 28, 2022, 6:30:50 PMJul 28

to

On July 20, pehou...@gmail.com wrote:

> back to present and

> the unused numbols vettor

> time

> slow

> down

> sped

> high

> slow high time good

> slow sped pepl good

> back to present and

> the unused numbols vettor

> time

> slow

> down

> sped

> high

> slow high time good

> slow sped pepl good

> high pepl time good

> good high time pepl

> tick tock goes clok

> grsp mind high time

> part slow down mind

> pepl plan part snow

> snow watr high time

>

> bob is a computer program for doing propositional reasoning on many simultaneous levels in three spatial

> and one temporal dimension

> bob works well on all regular graph coloring formalism with bounded degree being the major feature

> he runs in the background while i write in the foreground

> bob is my mind times speed one million

> i have a theory that

> monotone reason is linear

> bob is my proof that

> high level reason is monotone

> p=np for four word lines

> #p=np each solution satisfies

> common sense is monotone

> wisdom is deep monotone and conjunctive

Are you a product of the same DARPA AI lab as Ross Finlayson?
> good high time pepl

> tick tock goes clok

> grsp mind high time

> part slow down mind

> pepl plan part snow

> snow watr high time

>

> bob is a computer program for doing propositional reasoning on many simultaneous levels in three spatial

> and one temporal dimension

> bob works well on all regular graph coloring formalism with bounded degree being the major feature

> he runs in the background while i write in the foreground

> bob is my mind times speed one million

> i have a theory that

> monotone reason is linear

> bob is my proof that

> high level reason is monotone

> p=np for four word lines

> #p=np each solution satisfies

> common sense is monotone

> wisdom is deep monotone and conjunctive

--

Rich

Jul 29, 2022, 7:40:23 AMJul 29

to

i believe so

but

i have

as good as it gets

solved
the

P=NP=PSPACE=#P=#Q=QSPACE

equation for modest sizes

such as

may be needed for

mind

Jul 30, 2022, 5:41:52 PMJul 30

to

I'm only five foot eleven and a half inches tall though,

not six foot zero or six one, ....

My study is mathematics with physics second.

Sorry, no, it was long ago confirmed "Ross Finlayson"

is a troll, not a bot.

Clones, though, they're clones.

Sorry, I had to bite at "DARPA AI".

The Defence Advanced Research Projects Agency,

these days they made another one I forget what it's called.

Here "Ross Finlayson" is king of our trolls.

Also , "monotone quantified boolean formula"

are linearly decide-able.

Hey it was great reading some more about people

and the Physical Union.

"Ross Finlayson is king of our trolls".

Jul 31, 2022, 4:36:35 AMJul 31

to

If I could compile Bob, I could maybe count this chess problem here:

?- board_enum(X),

knight_enum_noattack_king(Y, X),

knight_enum_noattack_king(Z, X),

Y \== Z,

forall((king_move(X, A), on_board(A)),

(knight_move(Y, A); knight_move(Z, A))).

The result should be 32 when this gets counted. Right?

?- board_enum(X),

knight_enum_noattack_king(Y, X),

knight_enum_noattack_king(Z, X),

Y \== Z,

forall((king_move(X, A), on_board(A)),

(knight_move(Y, A); knight_move(Z, A))).

The result should be 32 when this gets counted. Right?

Jul 31, 2022, 4:42:10 AMJul 31

to

Here is a picture of solution Nr. 18:

Dogelog Player computing a Patt Situation

https://twitter.com/dogelogch/status/1553659518457896960

Dogelog Player computing a Patt Situation

https://www.facebook.com/groups/dogelog

Dogelog Player computing a Patt Situation

https://twitter.com/dogelogch/status/1553659518457896960

Dogelog Player computing a Patt Situation

https://www.facebook.com/groups/dogelog

Jul 31, 2022, 5:35:54 AMJul 31

to

This is more efficient, some symmetry breaking:

?- board_enum(X),

knight_enum_noattack_king(Y, X),

knight_enum_noattack_king(Z, X),

Y @< Z,

forall((king_move(X, A), on_board(A)),

(knight_move(Y, A); knight_move(Z, A)))).

The count is now only 16. Time to compute the same solution is now different:

/* Y \== Z, 32 Solutions */

% Wall 6196 ms, gc 11 ms, 2486273 lips

Solution Nr. 23 displayed

/* Y @< Z, 16 Solutions */

% Wall 4045 ms, gc 1 ms, 2471281 lips

Solution Nr. 11 displayed

?- board_enum(X),

knight_enum_noattack_king(Y, X),

knight_enum_noattack_king(Z, X),

forall((king_move(X, A), on_board(A)),

(knight_move(Y, A); knight_move(Z, A)))).

The count is now only 16. Time to compute the same solution is now different:

/* Y \== Z, 32 Solutions */

% Wall 6196 ms, gc 11 ms, 2486273 lips

Solution Nr. 23 displayed

/* Y @< Z, 16 Solutions */

% Wall 4045 ms, gc 1 ms, 2471281 lips

Solution Nr. 11 displayed

Jul 31, 2022, 7:59:33 AMJul 31

to

i should put on github butt

the form is followed by the q formula

the solving takes thousands of cpu cycles

p cnf 30 120

+1 +16 0

+2 +17 0

+3 +18 0

+4 +19 0

+5 +20 0

+6 +21 0

+7 +22 0

+8 +23 0

+9 +24 0

+10 +25 0

+11 +26 0

+12 +27 0

+13 +28 0

+14 +29 0

+15 +30 0

1 16 11 26 0

+1 16 +11 26 0

1 +16 11 +26 0

1 16 15 30 0

+1 16 +15 30 0

1 +16 15 +30 0

1 16 15 30 0

+1 16 +15 30 0

1 +16 15 +30 0

1 16 8 23 0

+1 16 +8 23 0

1 +16 8 +23 0

2 17 12 27 0

+2 17 +12 27 0

2 +17 12 +27 0

2 17 7 22 0

+2 17 +7 22 0

2 +17 7 +22 0

2 17 9 24 0

+2 17 +9 24 0

2 +17 9 +24 0

2 17 7 22 0

+2 17 +7 22 0

2 +17 7 +22 0

2 17 10 25 0

+2 17 +10 25 0

2 +17 10 +25 0

3 18 15 30 0

+3 18 +15 30 0

3 +18 15 +30 0

3 18 7 22 0

+3 18 +7 22 0

3 +18 7 +22 0

3 18 7 22 0

+3 18 +7 22 0

3 +18 7 +22 0

3 18 6 21 0

+3 18 +6 21 0

3 +18 6 +21 0

3 18 15 30 0

+3 18 +15 30 0

3 +18 15 +30 0

4 19 5 20 0

+4 19 +5 20 0

4 +19 5 +20 0

4 19 8 23 0

+4 19 +8 23 0

4 +19 8 +23 0

4 19 8 23 0

+4 19 +8 23 0

4 +19 8 +23 0

4 19 8 23 0

+4 19 +8 23 0

4 +19 8 +23 0

4 19 15 30 0

+4 19 +15 30 0

4 +19 15 +30 0

5 20 6 21 0

+5 20 +6 21 0

5 +20 6 +21 0

5 20 6 21 0

+5 20 +6 21 0

5 +20 6 +21 0

6 21 13 28 0

+6 21 +13 28 0

6 +21 13 +28 0

6 21 9 24 0

+6 21 +9 24 0

6 +21 9 +24 0

7 22 13 28 0

+7 22 +13 28 0

7 +22 13 +28 0

8 23 11 26 0

+8 23 +11 26 0

8 +23 11 +26 0

9 24 14 29 0

+9 24 +14 29 0

9 +24 14 +29 0

10 25 13 28 0

+10 25 +13 28 0

10 +25 13 +28 0

10 25 14 29 0

+10 25 +14 29 0

10 +25 14 +29 0

10 25 12 27 0

+10 25 +12 27 0

10 +25 12 +27 0
10 25 13 28 0

+10 25 +13 28 0

10 +25 13 +28 0

11 26 13 28 0

+11 26 +13 28 0

11 +26 13 +28 0

11 26 12 27 0

+11 26 +12 27 0

11 +26 12 +27 0

11 26 14 29 0

+11 26 +14 29 0

11 +26 14 +29 0

12 27 14 29 0

+12 27 +14 29 0

12 +27 14 +29 0

12 27 14 29 0

+12 27 +14 29 0

12 +27 14 +29 0

[p300_n15.veg 1]

1 (n 30 m 120) #c1 n the answer = 9 avg 1 variance 81 #P 300

q cnf 30 201

4 2 1 0

19 2 1 0

20 2 1 0

5 3 1 0

9 3 1 0

20 3 1 0

6 4 1 0

7 4 1 0

17 9 4 1 0

13 4 1 0

18 4 1 0

22 4 1 0

7 5 1 0

9 5 1 0

19 13 5 1 0

18 5 1 0

17 7 6 1 0

18 6 1 0

20 17 7 1 0

19 7 1 0

8 1 0

17 13 1 0

18 13 1 0

20 13 1 0

15 1 0

16 1 0

21 17 1 0

19 18 1 0

20 18 1 0

24 18 1 0

21 19 1 0

22 19 1 0

24 19 1 0

22 20 1 0

24 20 1 0

23 1 0

28 1 0

6 4 2 0

16 4 2 0

18 4 2 0

19 13 5 2 0

18 6 2 0

7 2 0

8 2 0

9 2 0

18 13 2 0

20 13 2 0

20 16 2 0

17 2 0

21 19 2 0

22 2 0

23 2 0

24 2 0

28 2 0

9 4 3 0

13 4 3 0

13 5 3 0

17 5 3 0

6 3 0

7 3 0

17 9 3 0

20 13 3 0

15 3 0

20 16 3 0

18 3 0

19 3 0

23 20 3 0

21 3 0

22 3 0

24 3 0

28 3 0

5 4 0

18 6 4 0

17 7 4 0

8 4 0

17 16 9 4 0

16 13 4 0

18 13 4 0

15 4 0

18 16 4 0

22 16 4 0

18 17 4 0

28 18 4 0

19 4 0

20 4 0

21 4 0

23 4 0

24 4 0

6 5 0

18 8 5 0

15 9 5 0

17 9 5 0

15 13 5 0

19 16 13 5 0

18 13 5 0

19 18 5 0

20 5 0

21 5 0

23 5 0

24 5 0

28 5 0

17 16 7 6 0

18 8 6 0
9 6 0

13 6 0

15 6 0

18 16 6 0

18 17 6 0

19 6 0

20 6 0

21 6 0

22 6 0

23 6 0

24 6 0

28 6 0

9 7 0

13 7 0

17 15 7 0

20 17 16 7 0

18 7 0

21 7 0

22 7 0

23 7 0

24 7 0

28 7 0

9 8 0

13 8 0

17 8 0

19 8 0

20 8 0

21 8 0

22 8 0

23 8 0

24 8 0

28 8 0

13 9 0

17 15 9 0

18 9 0

19 9 0

20 9 0

21 9 0

22 9 0

23 9 0

24 9 0

28 9 0

10 0

11 0

12 0

17 15 13 0

17 16 13 0

18 16 13 0

20 16 13 0

18 17 13 0

20 17 13 0

19 18 13 0

20 18 13 0

21 13 0

22 13 0

23 13 0

24 13 0

28 13 0

14 0

18 15 0

19 15 0

20 15 0

21 15 0

22 15 0

23 15 0

21 17 16 0

20 18 16 0

24 18 16 0

21 19 16 0

22 19 16 0

22 20 16 0

24 20 16 0

23 16 0

19 17 0

22 17 0

23 17 0

24 17 0

24 19 18 0

23 20 18 0

28 20 18 0

21 18 0

22 18 0

20 19 0

23 19 0

28 19 0

21 20 0

23 21 0

24 21 0

28 21 0

24 22 0

28 22 0

24 23 0

28 23 0

28 24 0

25 0

26 0

27 0

29 0

[p300_n15.veg 1 (t 300 z 0)(work 286 0 5289)] n 1 avg 1 variance 81 #P

[bigsums (tfiles 1 tforms 1) (numberp 300 zeromos 0)(retros 286 bigoh 0 Billion 5289)]

5289 inferences and 286 assumptions

daniel2380++

Jul 31, 2022, 8:03:40 AMJul 31

to

the form is a c3d5n15 regular coloring form

with 300 colorings of 15 vertices

daniel

with 300 colorings of 15 vertices

daniel

Jul 31, 2022, 8:20:25 AMJul 31

to

are both on github again

oneum features arbitrary randum interior bits

of prime numbers in 5 cpu cycles

bob solves all qbfs of pspace

daniel2380++

Jul 31, 2022, 9:40:58 AMJul 31

to

set theory foundation

includes n boolean variables for

set membership satisfaction

with at most 2^n members

daniel2380++

Jul 31, 2022, 10:08:56 AMJul 31

to

Still waiting for bobsmith.cpp solving

the chess problem. But nothing so far.

Or is the garbage below supposed to be related?

pehou...@gmail.com schrieb am Sonntag, 31. Juli 2022 um 13:59:33 UTC+2:

> On Sunday, July 31, 2022 at 5:35:54 AM UTC-4, Mostowski Collapse wrote:

> > This is more efficient, some symmetry breaking:

> > ?- board_enum(X),

> > knight_enum_noattack_king(Y, X),

> > knight_enum_noattack_king(Z, X),

> > Y @< Z,

> > forall((king_move(X, A), on_board(A)),

> > (knight_move(Y, A); knight_move(Z, A)))). r

the chess problem. But nothing so far.

Or is the garbage below supposed to be related?

pehou...@gmail.com schrieb am Sonntag, 31. Juli 2022 um 13:59:33 UTC+2:

> On Sunday, July 31, 2022 at 5:35:54 AM UTC-4, Mostowski Collapse wrote:

> > This is more efficient, some symmetry breaking:

> > ?- board_enum(X),

> > knight_enum_noattack_king(Y, X),

> > knight_enum_noattack_king(Z, X),

> > Y @< Z,

> > forall((king_move(X, A), on_board(A)),

Jul 31, 2022, 10:39:14 AMJul 31

to

one dozen cpu cycles per inference

i am glad you got bobsmith.cpp

check out preamble for compiler options

daniel2380++

Jul 31, 2022, 11:18:45 AMJul 31

to

here are some "under five hundred" problems

the #P is the answer

the #c is how many components in all answers

"the answer" below is the bit string length of the answer

n is number of variables

m is number of clauses

daniel2380++

[c3d5N240_0.veg 1]

1 (n 480 m 2040) #c3245599 n the answer = 25 avg 3245599 variance 625 #P 23168838

2 (n 480 m 2040) #c9698304 n the answer = 31 avg 6471951 variance 865 #P 1096665750

3 (n 480 m 2040) #c9420411 n the answer = 29 avg 7454771 variance 958 #P 405829686

4 (n 480 m 2040) #c8557507 n the answer = 28 avg 7730455 variance 1007 #P 265274250

5 (n 480 m 2040) #c7803378 n the answer = 31 avg 7745039 variance 1045 #P 1099352154

6 (n 480 m 2040) #c6149681 n the answer = 30 avg 7479146 variance 1070 #P 918246138

7 (n 480 m 2040) #c4665251 n the answer = 26 avg 7077161 variance 1083 #P 46042494

8 (n 480 m 2040) #c5474361 n the answer = 27 avg 6876811 variance 1094 #P 67533132

9 (n 480 m 2040) #c5796407 n the answer = 26 avg 6756766 variance 1102 #P 38909766

the #P is the answer

the #c is how many components in all answers

"the answer" below is the bit string length of the answer

n is number of variables

m is number of clauses

daniel2380++

[c3d5N240_0.veg 1]

1 (n 480 m 2040) #c3245599 n the answer = 25 avg 3245599 variance 625 #P 23168838

2 (n 480 m 2040) #c9698304 n the answer = 31 avg 6471951 variance 865 #P 1096665750

3 (n 480 m 2040) #c9420411 n the answer = 29 avg 7454771 variance 958 #P 405829686

4 (n 480 m 2040) #c8557507 n the answer = 28 avg 7730455 variance 1007 #P 265274250

5 (n 480 m 2040) #c7803378 n the answer = 31 avg 7745039 variance 1045 #P 1099352154

6 (n 480 m 2040) #c6149681 n the answer = 30 avg 7479146 variance 1070 #P 918246138

7 (n 480 m 2040) #c4665251 n the answer = 26 avg 7077161 variance 1083 #P 46042494

8 (n 480 m 2040) #c5474361 n the answer = 27 avg 6876811 variance 1094 #P 67533132

9 (n 480 m 2040) #c5796407 n the answer = 26 avg 6756766 variance 1102 #P 38909766

Aug 4, 2022, 11:57:24 AMAug 4

to