# Theorem: Monotone quantified boolean formula are linearly decidable

190 views

### Daniel Pehoushek

Jul 19, 2022, 2:38:30 AMJul 19
to
Plug zero for universal quantifications and one for existential quantifications then evaluate.
daniel 2380++

### Daniel Pehoushek

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:
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.

### Daniel Pehoushek

Jul 19, 2022, 6:04:19 AMJul 19
to
here is the most interesting line 89 of bob code 1000 lines
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*/

### Daniel Pehoushek

Jul 19, 2022, 6:09:25 AMJul 19
to
the theorem of the subject "monotone reason is linear"
shall be elementary memorization
daniel2380++

### Daniel Pehoushek

Jul 19, 2022, 6:29:18 AMJul 19
to
the +1 proof that god ezists
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*/

bignum& operator+=(bignum& j) {for(num k=zero;k<j.n.size();k++){when(k==n.size())n.add(zero);when(j.n[k])godezists(k);} return *this;}
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);
bignum& operator*=(num j){bignum*sum=getbignum();(*sum).n.clear();for(num g=zero;g<fifthtau+one;g++)when(j&ones[g]){
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]){
/*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 prinstringten(){nums rettles(times(sev,n.size()));bignum s(n);num r=zero;num gthree=zero;num y=zero;
joy fprinstringten(FILE*filem){nums rettles(times(sev,n.size()));bignum s(n);num r=zero;num gthree=zero;num y=zero;
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();}
}; // 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++

### Daniel Pehoushek

Jul 19, 2022, 12:11:51 PMJul 19
to
class godnum {nums n;joy godezists(num k){when(k==n.y)n.add(zero);when(++n[k]>>one){n[k]=zero;godezists(k+one);}}}
/*zero to infinity*/
daniel2380++

### Daniel Pehoushek

Jul 20, 2022, 8:07:39 AMJul 20
to
back to present and
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++

### Daniel Pehoushek

Jul 21, 2022, 7:49:56 PMJul 21
to
avoid negation and be well
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
built conjunctively

monotone reason is linear
bob is my proof that
high level reason is monotone
p=np for five 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
et cetera
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
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++

### Daniel Pehoushek

Jul 22, 2022, 8:34:07 PMJul 22
to
here is the most entertaining class in bob: bignum
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*/
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]){
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]){
/*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);

### Mostowski Collapse

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)

### Jeffrey Rubard

Jul 24, 2022, 6:17:46 PMJul 24
to
Have you heard of Kurt Goedel?
"I've heard of Kurt Gödel."
Well.

### Mostowski Collapse

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.

### Mostowski Collapse

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

### Mostowski Collapse

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

### Daniel Pehoushek

Jul 24, 2022, 9:00:49 PMJul 24
to
propositional math i see. interesting possibility...

#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)
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

### Daniel Pehoushek

Jul 25, 2022, 10:36:18 AMJul 25
to
so the solver translates bit encoded satisfiable assignments
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

### Mostowski Collapse

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

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.

### Daniel Pehoushek

Jul 25, 2022, 1:42:24 PMJul 25
to
monotone means with
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)
i like that you have lessthan
(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

what does plus look like? OR?
like that exponentiation?

### Mostowski Collapse

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?

### Mostowski Collapse

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?

### Mostowski Collapse

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

### Daniel Pehoushek

Jul 25, 2022, 8:06:41 PMJul 25
to
implication is bad for monotonicity

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

### Daniel Pehoushek

Jul 25, 2022, 8:10:04 PMJul 25
to
i believe bob is optimal on regular graph coloring
formulas which is very generl

### Daniel Pehoushek

Jul 25, 2022, 8:14:38 PMJul 25
to
to evaluate a quantification in monotone form
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...

### Daniel Pehoushek

Jul 26, 2022, 12:26:39 AMJul 26
to
co #c4295 answer length = 14 n 1 average 4295 variance 196 #a 10614 #i 0 (179259)) 9504
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

### Mostowski Collapse

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?

### Mostowski Collapse

Jul 26, 2022, 5:19:18 AMJul 26
to
Graphically WFC looks pretty neat:

Procedural generation from a single example
with WaveFunctionCollapse

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.

### Daniel Pehoushek

Jul 26, 2022, 9:34:35 AMJul 26
to
my solver is the fastest smallest correct most efficient solver in the world.
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

### Daniel Pehoushek

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 //**************************
usually two variables per Bob of height 2 and n high one and one high zero Bob
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 *********************
for high twos the soups would all have a third numbol inserted into numbols and
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)**************
for identity

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

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

num count; // one // how many in tree // thought********************************************
number of one bits in tree
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 ********** **********
temporary values for measuring space and what component

### Mostowski Collapse

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

I tried to compile Bob, and it said:
KEYBOARD ERROR: Press any key to continue

### Daniel Pehoushek

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
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
daniel2380++

### Rich D

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
> 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?

--
Rich

### Daniel Pehoushek

Jul 29, 2022, 7:40:23 AMJul 29
to
wow
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

### Ross A. Finlayson

Jul 30, 2022, 5:41:52 PMJul 30
to
Oh, they have those now?

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".

### Mostowski Collapse

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?

### Mostowski Collapse

Jul 31, 2022, 4:42:10 AMJul 31
to
Here is a picture of solution Nr. 18:

Dogelog Player computing a Patt Situation

Dogelog Player computing a Patt Situation

### Mostowski Collapse

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

### Daniel Pehoushek

Jul 31, 2022, 7:59:33 AMJul 31
to
send me your email for the current bobsmith.cpp
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++

### Daniel Pehoushek

Jul 31, 2022, 8:03:40 AMJul 31
to
the form is a c3d5n15 regular coloring form
with 300 colorings of 15 vertices
daniel

### Daniel Pehoushek

Jul 31, 2022, 8:20:25 AMJul 31
to
bobsmith.cpp and randumseven.cpp generator
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++

### Daniel Pehoushek

Jul 31, 2022, 9:40:58 AMJul 31
to
in my opinion
set theory foundation
includes n boolean variables for
set membership satisfaction
with at most 2^n members
daniel2380++

### Mostowski Collapse

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

### Daniel Pehoushek

Jul 31, 2022, 10:39:14 AMJul 31
to
bob does three trillion inferences per day at
one dozen cpu cycles per inference
i am glad you got bobsmith.cpp
check out preamble for compiler options
daniel2380++

### Daniel Pehoushek

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