Theorem: Monotone quantified boolean formula are linearly decidable

Daniel Pehoushek

unread,

Jul 19, 2022, 2:38:30 AM7/19/22

to

Plug zero for universal quantifications and one for existential quantifications then evaluate.
daniel 2380++

Daniel Pehoushek

unread,

Jul 19, 2022, 2:50:50 AM7/19/22

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

unread,

Jul 19, 2022, 6:04:19 AM7/19/22

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

unread,

Jul 19, 2022, 6:09:25 AM7/19/22

to

the theorem of the subject "monotone reason is linear"
shall be elementary memorization
daniel2380++

Daniel Pehoushek

unread,

Jul 19, 2022, 6:29:18 AM7/19/22

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);
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++

Daniel Pehoushek

unread,

Jul 19, 2022, 12:11:51 PM7/19/22

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

unread,

Jul 20, 2022, 8:07:39 AM7/20/22

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

unread,

Jul 21, 2022, 7:49:56 PM7/21/22

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

Daniel Pehoushek

unread,

Jul 22, 2022, 8:34:07 PM7/22/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]){
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);}}

Mostowski Collapse

unread,

Jul 24, 2022, 6:15:47 PM7/24/22

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

unread,

Jul 24, 2022, 6:17:46 PM7/24/22

to

Have you heard of Kurt Goedel?
"I've heard of Kurt Gödel."
Well.

Mostowski Collapse

unread,

Jul 24, 2022, 6:35:32 PM7/24/22

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

unread,

Jul 24, 2022, 6:38:51 PM7/24/22

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

unread,

Jul 24, 2022, 6:43:03 PM7/24/22

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

unread,

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

unread,

Jul 26, 2022, 6:58:41 PM7/26/22

to

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

Daniel Pehoushek

unread,

Jul 27, 2022, 6:34:36 AM7/27/22

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

unread,

Jul 28, 2022, 6:30:50 PM7/28/22

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

unread,

Jul 29, 2022, 7:40:23 AM7/29/22

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

unread,

Jul 30, 2022, 5:41:52 PM7/30/22

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

unread,

Jul 31, 2022, 4:36:35 AM7/31/22

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

unread,

Jul 31, 2022, 4:42:10 AM7/31/22

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

Mostowski Collapse

unread,

Jul 31, 2022, 5:35:54 AM7/31/22

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

unread,

Jul 31, 2022, 7:59:33 AM7/31/22

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

unread,

Jul 31, 2022, 8:03:40 AM7/31/22

to

the form is a c3d5n15 regular coloring form
with 300 colorings of 15 vertices
daniel

Daniel Pehoushek

unread,

Jul 31, 2022, 8:20:25 AM7/31/22

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

unread,

Jul 31, 2022, 9:40:58 AM7/31/22

to

in my opinion
set theory foundation
includes n boolean variables for
set membership satisfaction
with at most 2^n members
daniel2380++

Mostowski Collapse

unread,

Jul 31, 2022, 10:08:56 AM7/31/22

P=NP=#P=#Q=PSPACE=QSPACE for modest sizes
common sense is monotone
wisdom is deep and monotone
each solution is satisfying (#P=NP)
#solutions = #questions (#P=#Q)
monotone reason is linear
universal truth is quadratic monotone and conjunctive

// Solve all QBFs in ten lines of code
// bit by bit linear transformation
// from models into questions
// P=NP for modest sizes
joy plan(num v, numnums& s) {
when(set.size()==zero || vee == env::N() ) return;
numnums l;numnums r;split(v,s,l,r);s.setsize(zero);/*bob mastermind of ordinary truth*/
plan(v+one,l);plan(v+one,r);juggle (v,l,r);
for(num g=zero;g<l.size();g++){ezis(*(l[g]),v);s.add(l[g]);}l.setsize(zero);
for(num g=zero;g<r.size();g++){univ(*(r[g]),v);s.add(r[g]);}r.setsize(zero);}

joy juggle (num v, numnums& l, numnums& r) {
if(l.size()==zero){for(num g=zero;g<r.size();g++)l.add(r[g]);r.setsize(zero);return;}
when(vee == env::N()) return;
numnums al;numnums ar;split(v+one,l,al,ar);l.setsize(zero);
numnums bl;numnums br;split(v+one,r,bl,br);r.setsize(zero);
juggle(v+one,al,bl);juggle(v+one,ar,br);
for(num g=zero;g<al.size();g++) l.add(al[g]); for(num g=zero;g<ar.size();g++) l.add(ar[g]);
for(num g=zero;g<bl.size();g++) r.add(bl[g]); for(num g=zero;g<br.size();g++) r.add(br[g]); }

joy zerotoone /*bit is on*/(nums& s, num b) { (s[b >> five] += (ones[b & fifthtau]));} //
num be /*is bit on*/(nums& s, num b) { return (s[b >> five] & (ones[b & fifthtau]));} //
joy ezis(nums& s, num b) { s[b >> five] &= zeroes[b & fifthtau]; } //
joy univ(nums& s, num b) { s[b >> five] & ones[b & fifthtau]; } //
joy split /*leftright around bit*/(num b, numnums& s, numnums& l, numnums& r) // left right on bit b
{for (num g = zero; g < s.size(); g++) if (be((*s[g]), b)) r.add(s[g]); else l.add(s[g]); } // oh of s.size()

num b=0; num p=2; // 5 cycles per quality random bit (prime returns a fifteen bit prime)
inline num oneum() { if (p<four<<++b) {p=prime(); b=one;} (one<<b&p) ? one:zero; }

Rich D

unread,

Aug 5, 2022, 5:30:39 PM8/5/22

to

On August 5, pehou...@gmail.com wrote:
> P=NP=#P=#Q=PSPACE=QSPACE for modest sizes
> common sense is monotone
> wisdom is deep and monotone
> each solution is satisfying (#P=NP)
> #solutions = #questions (#P=#Q)
> monotone reason is linear
> universal truth is quadratic monotone and conjunctive
> // Solve all QBFs in ten lines of code

Given 12 gold coins, including one counterfeit.
Label them A, B, ... L
Given a balance scale.

Three weightings are performed, as follows:
{A,B,C,D} vs {E,F,G,H}: left side heavy
{C,D,F,G} vs {E,I,J,K}: left side heavy
{C} vs {D}: balanced

Which one is counterfeit, is it lighter or heavier than the legitimates?

Formulate this problem as QBF - what does bob say?
Generalize to N coins. What's the largest N bob can handle?

--
Rich

Daniel Pehoushek

unread,

Aug 7, 2022, 2:43:08 AM8/7/22

Daniel Pehoushek

unread,

Aug 21, 2022, 4:12:49 PM8/21/22

to

i believe this theorem is news

monotone theorem of cognition

all quantified monotone
boolean and or forms are
linearly solvable and decidable.

just plug 1 for existentials and
0 for universals then evaluate.
this theorem derived from #P=#Q:
the number of satisfying solutions equals
the number of valid quantifications.

when words have monotone definitions
then
a few monotone words
look like common sense

daniel2380++

Daniel Pehoushek

unread,

Aug 21, 2022, 5:01:24 PM8/21/22

to

honest men are always smart
daniel2380++

Rich D

unread,

Aug 22, 2022, 2:24:57 PM8/22/22

to

On August 21, pehou...@gmail.com wrote:
> honest men are always smart

But not women -

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

--
Rich

Rich D

unread,

Aug 22, 2022, 2:31:55 PM8/22/22

to

On August 19, pehou...@gmail.com wrote:
>>> > > clause learning in #sat is incorrect and gives erroneous counts
>
>>>> Counts of what, exactly?
>

>>> #sat is the problem of counting satisfying boolean assignments
>

> for two years in a row
> model counting competition 2021
> model counting competition 2022
> bob is the only correct program

Competition, hmmm....

If the number of solutions is exponential, how do the judges know
the right answer, for large problems?

It's akin to a traveling salesman competition - no one knows the optimal
solution, so how do they judge the entrants?

--
Rich

Daniel Pehoushek

unread,

Aug 22, 2022, 4:04:21 PM8/22/22

to

some answers indeed have many bits
all are solvable
some are solvable in one day
when a program is correct on small cases try larger cases
judges have to be smart about small enough
daniel2380++

Daniel Pehoushek

unread,

Aug 22, 2022, 8:15:54 PM8/22/22

to

about my writing
i use the smallest alphabet i have available
to communicate in clausal form.
my alphabet is coded in five bits.
bobs source code is in monotone form 1000 lines.
daniel2380++

Daniel Pehoushek

unread,

Aug 23, 2022, 9:11:53 AM8/23/22

to

honest men are always smart

but dishonest men are
often confused

as proofs develop
truth often wins
and honesty
prevails

Daniel Pehoushek

unread,

Aug 23, 2022, 9:49:08 AM8/23/22

to

//first five lines of bob
typedef unsigned long num;
const num one = (num)true;
const num zero = one>>one; // one down one bit is zero
const num two = one+one+(one>>one); // two is one plus one plus zero // zero counts most cleanly //
const num three = two+one;

as for np=pspace
i point uselessly to my alphabet
+abcdefghijklmnopqrstuvw yz
twenty seven letters to write

honest men are always smart
but dishonest men are
often confused

as proofs develop
truth often wins
and honesty
prevails

if unbounded clause learning
is wrong when doing #sat
then it is wrong when doing sat
then clause learning is wrong
and sat==qbf (np==pspace)

my modest sizes equation still holds
p=np=pspace=#p=#q=qspace is truth
and for large just too big for bob
np=pspace=#p=#q=qspace is truth

Daniel Pehoushek

unread,

Aug 23, 2022, 10:08:31 AM8/23/22

to

honest men are always smart
but dishonest men are
often confused

as proofs develop
truth often wins
and honesty
prevails

if unbounded clause learning
is wrong when doing #sat
then it is wrong when doing sat
then clause learning is wrong
and sat==qbf (np==pspace)

#p=#q number of information equals number of question
#p=np each solution is satisfying
qbf is more than polynomial
monotone qbf is linear

my modest sizes equation still holds

p=np=pspace=#p=#q=qspace is bobs truth

and for large just too big for bob

np=pspace=#p=#q=qspace is just truth

avoid negation and be well
daniel2380++

ps random
the empty set may be created from
a set containing only the empty set
by removing that from the set

Daniel Pehoushek

unread,

Aug 23, 2022, 1:21:20 PM8/23/22

to

matter is monotone

about my writing
i use the smallest alphabet
i have available to communicate
in clausal form
my alphabet is coded
in five bits
bobs source code is
in monotone form 1000 lines
//first five lines of bob
typedef unsigned long num;

const num one = (num)true; // not true is constrained to be zero by defining true to be one

const num zero = one>>one; // one down one bit is zero
const num two = one+one+(one>>one); // two is one plus one plus zero // zero counts most cleanly //
const num three = two+one;

as for np=pspace
i point uselessly to my alphabet
+abcdefghijklmnopqrstuvw yz
twenty seven letters to write

honest men are always smart
but dishonest men are
often confused

as proofs develop
truth often wins
and honesty
prevails

that bob is correct truth on all inputs
shall propagate around the community
clause learning in bob is bounded
there are zero other clause learning programs
that are correct because of Carry Bit Validity
while counting during component analysis
bob uses hand built bignum data structures
to order the results trees
bignum addone has a proof of correctness

if unbounded clause learning
is wrong when doing #sat
then it is wrong when doing sat
then clause learning is wrong
and sat==qbf (np==pspace)

#p=#q number of information equals number of question
#p=np each solution is satisfying
qbf is more than polynomial
monotone qbf is linear

matter is monotone

my modest sizes equation still holds
p=np=pspace=#p=#q=qspace is bobs truth
and for large just too big for bob
np=pspace=#p=#q=qspace is just truth

that is large and immodestly stated

avoid negation and be well
daniel2380++

ps random
the empty set may be created from
a set containing only the empty set
by removing that from the set

rayoneum generates random in five cpu cycles
used to generate millions of coloring formulas
ninth degrees are toughys that bob solves well

Daniel Pehoushek

unread,

Aug 23, 2022, 2:02:17 PM8/23/22

to

to order rigorous component result trees

bignum addone has a proof of correctness

if unbounded clause learning
is wrong when doing #sat
then it is wrong when doing sat
then clause learning is wrong
and sat==qbf (np==pspace)

theorems to my credit
load balanced parallelism is with globally accessible local task stacks
vision is nlogn with +abcd recursion

#p=#q number of information equals number of question

pattern recognition is n/m time with mlogm space
most d regular graphs are 1+sqrt(d) colorable

#p=np each solution is satisfying

#q=qspace: #allqbfs equals universal monotone property in dnf or cnf
qbf is more than polynomial as the q cnf n m form may have large m
monotone qbf is linear in the n+m of the qbf
matter is mostly monotone

my modest sizes equation still holds
p=np=pspace=#p=#q=qspace is bobs truth
and for large just too big for bob
np=pspace=#p=#q=qspace is just truth
that is large and immodestly stated

be well and avoid negation and be well

Rich D

unread,

Aug 23, 2022, 2:21:39 PM8/23/22

to

On August 23, pehou...@gmail.com wrote:
> //first five lines of bob
> typedef unsigned long num;
> const num one = (num)true;
> const num zero = one>>one; // one down one bit is zero
> const num two = one+one+(one>>one); // two is one plus one plus zero // zero counts most cleanly //
> const num three = two+one;

Counting to three doesn't strike me as profound.
bob would be more impressive if he could count the reals -

> if unbounded clause learning
> is wrong when doing #sat
> then it is wrong when doing sat
> then clause learning is wrong
> and sat==qbf (np==pspace)

What's the difference between sat and #sat?

> my modest sizes equation still holds
> p=np=pspace=#p=#q=qspace is truth
> and for large just too big for bob
> np=pspace=#p=#q=qspace is truth

What's the largest composite bob can factor?

> avoid negation and be well

Avoiding negation nullifies a large territory of logic.
Our digital world would not exist without negation.
AND and OR gates are insufficient -

--
Rich

Daniel Pehoushek

unread,

Aug 23, 2022, 2:33:56 PM8/23/22

to

On Tuesday, August 23, 2022 at 2:21:39 PM UTC-4, rdelan...@gmail.com wrote:
> On August 23, pehou...@gmail.com wrote:
> > //first five lines of bob
> > typedef unsigned long num;
> > const num one = (num)true;
> > const num zero = one>>one; // one down one bit is zero
> > const num two = one+one+(one>>one); // two is one plus one plus zero // zero counts most cleanly //
> > const num three = two+one;
> Counting to three doesn't strike me as profound.

i got constant zero from truth without minus or negation
very profound

> bob would be more impressive if he could count the reals -

see bignum in bob for foundations of correct counting in a data structure

> > if unbounded clause learning
> > is wrong when doing #sat
> > then it is wrong when doing sat
> > then clause learning is wrong
> > and sat==qbf (np==pspace)
> What's the difference between sat and #sat?

sat halts when the count of solutions gets to one
#sat counts all solutions
in bob when the #P answer is computable then
all qbfs of the original form are decidable with bob
under five hundred variables generally

> > my modest sizes equation still holds
> > p=np=pspace=#p=#q=qspace is truth
> > and for large just too big for bob
> > np=pspace=#p=#q=qspace is truth
> What's the largest composite bob can factor?

48 or 64 bits answers are solvable

> > avoid negation and be well
> Avoiding negation nullifies a large territory of logic.
> Our digital world would not exist without negation.
> AND and OR gates are insufficient -

but
avoiding negation is in principle
good for coherent legible writing
>
>
> --
> Rich

Rich D

unread,

unread,

Aug 28, 2022, 9:11:41 AM8/28/22

to

On Saturday, August 27, 2022 at 6:28:59 PM UTC-4, rdelan...@gmail.com wrote:
> On August 27, pehou...@gmail.com wrote:
> >> The theorem derives from #P=#Q.
> > bobs monotone cnf describes propertys of the input
> > bobs monotone dnf describes good questions of the input
> What is the definition of a good question?
> > NP=PSPACE=#P may be the whole truth being uncovered by the community
> Is it possible to determine the number of valid solutions
> non-constructively, i.e. without demonstrating any particular solution?

only closed forms but
in general practically
all details of all components
must make an appearance
on the solver stack

> > rayoneum is an optimal random bit generator
> It uses the decay reactions of a radioactive element
> as a source?

five cpu cycles man!

>
> --
> Rich

unread,

Aug 29, 2022, 6:11:52 AM8/29/22

to

a quantification binds variables to "forall" or "exists"
such as: forall a exists b (a or b)

on n variables there are 2^n possible quantifications

bob finds all valid quantifications
in linear time from a disjunction
of all satisfying solutions

stages of bob
p cnf n m : original formula
p dnf n #P : disjunction of all solutions
q dnf n #P : disjunction of valid quantifications
q cnf n M :conjunction of monotone property

+++

as for five clock cycles per random bit
rayoneum competes favorably with all other rbgs (random bit generators)
using the same amount of clock time per random bit, bob wins...
daniel2380++

Daniel Pehoushek

unread,

Aug 29, 2022, 12:44:19 PM8/29/22

to

for p valevolent
dark energy by e=mlogmc^2
dark matter by Fr^2 = G m1m2 logm1logm2
daniel2380++

Jeff Barnett

unread,

Daniel Pehoushek

unread,

Sep 6, 2022, 4:22:44 PM9/6/22

to

of course it was general.
bob is correct on all inputs.

monotone quantified boolean formula are linearly solvable
is just a theorem arising from the work.
daniel2380++

Rich D

unread,

Sep 7, 2022, 3:36:08 PM9/7/22

to

On September 6, pehou...@gmail.com wrote:
>>> bob was the only correct program for model counting competition 2021 and 2022.
>>> be well and avoid negation
>> Did the competition include negated variables in the problems?
>

> of course it was general.
> bob is correct on all inputs.

You said bob avoids negation.

--
Rich

Daniel Pehoushek

unread,

Sep 7, 2022, 4:59:21 PM9/7/22

to

bob solves general boolean formulas that are in conjunctive normal form.
the final formula that decides validity of all 2^n possible quantifications is monotone.

be well and avoid negation,
daniel2380++