Pspace magic transform to Qspace, solving all QBFs

[Daniel Pehoushek]

Pspace transform to Qspace, solving all QBFs

given the set of satisfying models (bit encoded)
produce the set of satisfying quantifications
in linear transformation from pspace in dnf
to qspace in dnf, thus solving pspaces.

this transform solves all qbfs, in bit coded form.
the input is any pspace in dnf,
the output is qspace in dnf.
one dozen lines of code.
daniel2380+++

entry: plan(0, all_models); out: all_quantifications.
// transform all boolean models into all true questions
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); }
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); left.setsize(zero);
numnums bl; numnums br; split(vee + one, right, bl, br); right.setsize(zero);
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 zerotoone /*bit is on*/(nums& s, num b) { (s[b >> five] += (ones[b & fifthtau])); } //
static num be(nums& s, num b) { return (s[b >> five] & (ones[b & fifthtau])); }
static joy ezis(nums& s, num b) { s[b >> five] &= zeroes[b & fifthtau]; }
static 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]); } //

[Daniel Pehoushek]

#P=#Q was the genesis of Pspace=Qspace, in 1997, 2002.
The number of satisfying models equals the number of valid quantifications.

Published in 2002 at Satisfiability Conference, page one...

Solving All qbfs in time proportional to solving one qbf,
the transform collapses "difficulty" of the hierarchy.

Other results:
Monotone qbfs are linearly decidable.
Monotone reason is linear.

#P=NP: Each solution is satisfying.

For modest size, P=NP=Pspace=#P=#Q=Qspace.

There is a quadratic transform from monotone dnf to monotone cnf,
producing "universal truth" in conjunctive normal form.

numsat.cpp is 1000 lines of code.

daniel2380++

[Daniel Pehoushek]

this class is a goldmine for logic
the input solutions are boolean models
the output solves all qbfs by assignment evaluation
daniel2380+++

class allqbfs; // leftright ezistential property sorting system bit by bit bobs general algorithm thinking is entirely andor operations
class allqbfs { // linear transform satisfiable solutions into all qbfs solutions divine consciousness algorithm of skull bone //
public: // think: call bob of p to produce q propertys over p hypothetical truths of mind ambient generality //
static set<allqbfs*> qvars; // meta vars identity quantifiers of the n p variables //
static numnums qforms; // ezistential truths (ors of few variables) among identity of p formula //
static numnums solutions; // the finite set of all satisfying solutions then all valid quantifications then dnf to cnf //
numnums forms; num mark; // ezistential truths location j has a temporary mark during dnftocnf //
allqbfs(num v):forms(zero),mark(zero){} ~allqbfs(){forms.clear();} //
static joy delqforms() { //
for (num g = zero; g < qforms.size(); g++) { putnums(qforms[g]); qforms[g] = (nums*)zero; } qforms.clear(); //
for (num g = zero; g < qvars.size(); g++) { (*qvars[g]).forms.clear(); delete (qvars[g]); } qvars.clear(); } //
num review(num r) { // scan for all true variables //
for (num j = zero; j < forms.size(); j++) { num k = zero; num s = (*forms[j]).size(); //
when(s < r) { for (k = zero; k < s; k++) { when((*qvars[(*forms[j])[k]]).mark == zero) pray/*prayercounter++*/ } when(k == s) return one; } //
} return zero; } //
static joy publish(nums& phrase) { // add iff nay already written as clauses grow the cost of this operation grows //
num write = one; //
for (num j = zero; j < phrase.size(); j++) { (*qvars[phrase[j]]).mark = one; } //
when((*qvars[phrase[minus(phrase.size(), one)]]).review(phrase.size())) write = zero; //
for (num j = zero; j < phrase.size(); j++) { (*qvars[phrase[j]]).mark = zero; } //
when(write) {nums* nc = getnums(phrase.size()); // as yet unwritten //
for (num j = zero; j < phrase.size(); j++) (*nc).add(phrase[j]); qforms.add(nc); //
when((qforms.size() & thetenthtau) == zero) prin("*"); //
for (num j = zero; j < phrase.size(); j++) { (*qvars[phrase[j]]).forms.add(nc); } } } //

// transform all boolean models into all true questions

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); left.setsize(zero);
numnums bl; numnums br; split(vee + one, right, bl, br); right.setsize(zero);
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); }
static joy zerotoone /*bit is on*/(nums& s, num b) { (s[b >> five] += (ones[b & fifthtau])); } //

static num be(nums& s, num b) { return (s[b >> five] & (ones[b & fifthtau])); } //
static joy ezis(nums& s, num b) { s[b >> five] &= zeroes[b & fifthtau]; } //

static 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]); } //

static joy essay(num wordnum, numnums& qbfs, nums& phrase) { // architecture of written high level thought
when(wordnum==qvars.size())return;//the essence of good language is modestly sized monotone phrases
when(qbfs.size() == zero) { publish(phrase); return; } // check for subsumption
numnums left; numnums right; split(wordnum, qbfs, left, right); essay(wordnum + one, left, phrase); // essay ezistentially
phrase.add(wordnum); essay(wordnum + one, right, phrase); phrase.slop(); } // finish wordnum
static joy wisdom(FILE* logfile, numnums& qclauses)
{for (num j = one; j < qforms.size() + one; j++) { //
fprin(logfile, "\n"); nums& phrase = (*qforms[minus(qforms.size(), j)]); num s = phrase.size(); //
for (num g = one; g < one + s; g++) { fprin(logfile, "%u ", (one + phrase[minus(s, g)])); } fprin(logfile, "0"); } } //
};// tau three

[Daniel Pehoushek]

class allqbfs performs real general intelligence on cnfs.
transform pspace in dnf to qspace first in q dnf then q cnf
high level thought is
printed in q cnf by essay with wisdom

be well and avoid negation
daniel2380+++

[Daniel Pehoushek]

numsat.cpp is 1000 lines of equational code.
the stages of transformation go from p cnf to p dnf to q dnf to q cnf.
the last stage outputs the universal truth (set propertys) of the p cnf.

other news: clause learning is wrong while solving #sat.
that is my christmas gift to the logic community,
to avoid years of wasted research time,

be well and avoid negation,
daniel2380+++

[Daniel Pehoushek]

The most trivial clause learning gives wrong answers for #sat (number satisfiability).
This leads to the conclusion that clause learning is at best incomplete.

There are zero correct #sat programs that do clause learning.
Big news in Logic.

[Rich D]

On January 23, pehou...@gmail.com wrote:
> The most trivial clause learning gives wrong answers for #sat (number satisfiability).
> This leads to the conclusion that clause learning is at best incomplete.

What is clause learning?

--
Rich

[Daniel Pehoushek]

from wiki:
Algorithm
Conflict-driven clause learning works as follows.

Select a variable and assign True or False. This is called decision state. Remember the assignment.
Apply Boolean constraint propagation (unit propagation).
Build the implication graph.
If there is any conflict
Find the cut in the implication graph that led to the conflict
Derive a new clause which is the negation of the assignments that led to the conflict
Non-chronologically backtrack ("back jump") to the appropriate decision level, where the first-assigned variable involved in the conflict was assigned
Otherwise continue from step 1 until all variable values are assigned.

+++

However, the most trivial clause learning gives undercounts,
so the method's completeness is in doubt.

In the model counting competitions 2021 2022
numsat (formerly bob) was the only correct
solver for #sat.
daniel2380+++

[Daniel Pehoushek]

from wiki:
Completeness
DPLL is a sound and complete algorithm for SAT. CDCL SAT solvers implement DPLL, but can learn new clauses and backtrack non-chronologically. Clause learning with conflict analysis affects neither soundness nor completeness. Conflict analysis identifies new clauses using the resolution operation. Therefore, each learnt clause can be inferred from the original clauses and other learnt clauses by a sequence of resolution steps. If cN is the new learnt clause, then ϕ is satisfiable if and only if ϕ ∪ {cN} is also satisfiable. Moreover, the modified backtracking step also does not affect soundness or completeness, since backtracking information is obtained from each new learnt clause.[5]

+++
i argue with this point

If cN is the new learnt clause, then ϕ is satisfiable if and only if ϕ ∪ {cN} is also satisfiable.

because learning gives wrong model counts, so learning is wrong while solving #sat.

since it is wrong for #sat, it is also wrong for sat and unsat.
Really big news in logical circles.
clause knowing is right, learning is wrong.

be well and avoid negation.
daniel2380+++

[Daniel Pehoushek]

in class allqbfs
any pspace in disjunctive normal form
linearly transforms to qspace in dnf

with quadratic transform essay and
wisdom output a monotone conjunctive normal form
that describes all general properties of the input

high level general real intelligence in 50 lines of code

but the other big news is that
clause knowing is right and clause learning is wrong

[Rich D]

On January 31, pehou...@gmail.com wrote:
>>> In the model counting competitions 2021 2022
>>> numsat (formerly bob) was the only correct
>>> solver for #sat.

How do they know the correct solutions, if the problems
are NP? It's like a traveling salesman competition.

> but the other big news is that
> clause knowing is right and clause learning is wrong

How does one know the clause, without learning the
clause? My experience says that learning precedes
knowing; necessary but not sufficient.


--
Rich

[Daniel Pehoushek]

On Wednesday, February 1, 2023 at 3:25:53 PM UTC-5, rdelan...@gmail.com wrote:
> On January 31, pehou...@gmail.com wrote:
> >>> In the model counting competitions 2021 2022
> >>> numsat (formerly bob) was the only correct
> >>> solver for #sat.
> How do they know the correct solutions, if the problems
> are NP? It's like a traveling salesman competition.

numsat is a correct program
so they may use that to check all programs

> > but the other big news is that
> > clause knowing is right and clause learning is wrong
> How does one know the clause, without learning the
> clause? My experience says that learning precedes
> knowing; necessary but not sufficient.

see numsat.cpp for full details
about this enigmatic condition

upon input all feasible resolvents are computed
so knowing the resolvent while solving is right
but i claim that learning the resolvent is wrong
while solving

stretching theory says what is correct for #sat
is also true for sat and unsat solving.
so this is really big news

be well and avoid negation

bowing to the conjunctive general
theory of monotone wisdom
daniel2380+++

[Rich D]

On February 2, Daniel Pehoushek wrote:
>>>> In the model counting competitions 2021 2022
>>>> numsat (formerly bob) was the only correct
>>>> solver for #sat.
>
>> How do they know the correct solutions, if the problems
>> are NP? It's like a traveling salesman competition.
>
> numsat is a correct program
> so they may use that to check all programs

How can you be sure?

At last Friday's seance, I summoned Kurt Godel, and asked
him about this. He said he couldn't decide.

--
Rich

[Daniel Pehoushek]

numsat has two ways to compute model counts.

one by one enumeration without components,
and also components with bignum multiply.

bignum multiply is only used in one function.
both ways get the same number.

when the boolean formulas are modestly sized they can be solved completely.

be well and avoid negation

in accordance with
general monotone theory,
daniel2380+++

[Daniel Pehoushek]

here is class allqbfs for solving pspace in disjunctive normal form.
correct general boolean intelligence, wisdom is output in conjunctive normal form.

when(qbfs.size() == zero) { publish(phrase); return; } // check for subsumption
when(wordnum==qvars.size())return;//the essence of good language is modestly sized monotone phrases
numnums left; numnums right; split(wordnum, qbfs, left, right); essay(wordnum + one, left, phrase); // essay ezistentially
phrase.add(wordnum); essay(wordnum + one, right, phrase); phrase.slop(); } // finish wordnum
static joy wisdom(FILE* logfile, numnums& qclauses)
{ for (num j = one; j < qforms.size() + one; j++) { //
fprin(logfile, "\n"); nums& phrase = (*qforms[minus(qforms.size(), j)]); num s = phrase.size(); //

for (num g = zero; g < s; g++) { fprin(logfile, "%u ", (one + phrase[g])); } fprin(logfile, "0"); } } //
};// tau three
numnums allqbfs::solutions; // sev is thirdtau three is second
set<allqbfs*> allqbfs::qvars; //
numnums allqbfs::qforms; //

[Daniel Pehoushek]

flawed false poem about Godel's Complete Theory?
Here's a flawed false poem about Gödel's Completeness Theorem:

In the world of math, Gödel made his fame
With a theorem that bore his name
Complete and sound, it did attest
That every statement could be expressed

In symbols clear and logical rules
Without ambiguity, like a pack of tools
And with a proof so elegant and grand
It made mathematicians understand

But alas! This theorem had a flaw
That Gödel never foresaw
It meant that some statements were true
But could never be proved to be so, boo-hoo!

So let us beware of Gödel's theorem
For it undermines our certainty's scheme
And reminds us that even in math's perfection
There are limits to our comprehension.

While this poem has some elements of truth, it contains a fundamental flaw. Gödel's completeness theorem is actually a statement about first-order logic, and it does not imply that every statement can be expressed in that logic. Instead, it says that every semantically valid formula of first-order logic is provable in a suitably powerful logical system.

The incompleteness theorem, on the other hand, is the one that implies that there are true statements that cannot be proven within a given logical system. However, the poem confuses the two theorems and attributes the incompleteness result to the completeness theorem.

[Rich D]

On February 27, Daniel Pehoushek wrote:
> Here's a flawed false poem about Gödel's Completeness Theorem:
>
> In the world of math, Gödel made his fame
> With a theorem that bore his name
> Complete and sound, it did attest
> That every statement could be expressed

> But alas! This theorem had a flaw
> That Gödel never foresaw
> It meant that some statements were true
> But could never be proved to be so, boo-hoo!
> So let us beware of Gödel's theorem
> For it undermines our certainty's scheme
> And reminds us that even in math's perfection
> There are limits to our comprehension.
>
> While this poem has some elements of truth, it contains a fundamental flaw. Gödel's
> completeness theorem is actually a statement about first-order logic, and it does not
> imply that every statement can be expressed in that logic. Instead, it says that every
> semantically valid formula of first-order logic is provable in a suitably powerful logical system.
>
> The incompleteness theorem, on the other hand, is the one that implies that there are
> true statements that cannot be proven within a given logical system. However, the
> poem confuses the two theorems and attributes the incompleteness result to the completeness theorem.

Well, it's a poem, and there's something called poetic license.

Ask her to write an an essay on the difference between Godel's completeness
and incompleteness theorems.

--
Rich

[Daniel Pehoushek]

Gödel's completeness and incompleteness theorems are two significant results in mathematical logic that deal with the limits of formal systems in describing mathematical truths. In this essay, we will explore the difference between these two theorems and their implications for our understanding of mathematical logic.

Gödel's completeness theorem states that any consistent formal system capable of expressing a certain amount of arithmetic is complete. This means that every statement that is true within the system can be proven within the system. The completeness theorem was proven by Gödel in 1929 and is considered to be one of the most important results in mathematical logic.

The completeness theorem has significant implications for our understanding of mathematical logic. It means that we can use formal systems to prove all true statements within a certain domain of mathematics. For example, if we are working within the domain of arithmetic, then we can use a formal system to prove every true statement within that domain.

However, Gödel's incompleteness theorem shows that there are limits to what formal systems can accomplish. The incompleteness theorem states that any consistent formal system that is powerful enough to express arithmetic must contain statements that are true but cannot be proven within the system. In other words, there are true statements that exist beyond the reach of any formal system.

The incompleteness theorem has significant implications for our understanding of the limits of mathematical knowledge. It means that there will always be true statements that cannot be proven within a formal system, and thus, there will always be gaps in our understanding of mathematics. Gödel's incompleteness theorem has been called one of the most important results in the history of mathematics, and it has had a profound impact on the philosophy of mathematics.

To summarize, Gödel's completeness theorem states that every true statement within a formal system can be proven within that system, while Gödel's incompleteness theorem shows that there are always true statements that exist beyond the reach of any formal system. These theorems have profound implications for our understanding of mathematical logic and the limits of mathematical knowledge.

[Rich D]

On February 28, Daniel Pehoushek wrote:
>>> While this poem has some elements of truth, it contains a fundamental flaw. Gödel's
>>> completeness theorem is actually a statement about first-order logic, and it does not
>>> imply that every statement can be expressed in that logic. Instead, it says that every
>>> semantically valid formula of first-order logic is provable in a suitably powerful logical system.
>>> The incompleteness theorem, on the other hand, is the one that implies that there are
>>> true statements that cannot be proven within a given logical system. However, the
>>> poem confuses the two theorems and attributes the incompleteness result to the
>>> completeness theorem.
>

>> Ask her to write an an essay on the difference between Godel's completeness
>> and incompleteness theorems.
>

> In this essay, we will explore the difference between these two theorems and their
> implications for our understanding of mathematical logic.

> .... To summarize, Gödel's completeness theorem states that every true statement

> within a formal system can be proven within that system, while Gödel's
> incompleteness theorem shows that there are always true statements that exist
> beyond the reach of any formal system.

?
Is this not a contradiction?
Between ChatGirl and myself, one of us is confused -

--
Rich

[Ross Finlayson]

It's not "any" formal system to which GIT's apply, where, those with
"universal axiomatization" have it doesn't follow, and, those with
"null axiomatization" have it doesn't follow, so, there are unfounded assertions
there otherwise, of what's "so".

Then, reading of Goedel's theorems, make for there _are_ objects outside
the ordinary system, that are extra-ordinary, where of course Goedel's
theorems are about ordinary, or well-founded, arithmetizations, of
ordinary, well-founded, axiomatic systems' languages' objects.

Then it makes sense to place an object "infinity" and "universe".


Then, extra-ordinary logics, about the Goedel's implicature of either
consistency or completeness and not both, for ordinary systems,
gets into why there is dually-self-infraconsistency what any,
..., "theory of everything, true", _must_ be.

That there is one is often attributed to the G-dhead or Absolute.
That there is an "everything, true" though is as entirely evident,
because there's anything at all. Also it would be perfect that
as far as it's perfect, it's Perfection's. I.e., insofar as it's any
good, G-d has one already.


I was leafing through Nozick's Philosophical Explanations the other day,
about page 115 there's a section "why is there something instead of nothing?",
and it's not just a coincidence that the Bible begins with "there was nothing,
then there was something", and about in the middle or Matthew "in the beginning,
there was the word", anyways he quotes a fellow about something like "there
are four things never to question, what's above and below and what's before and after".
So, of course the Bible has that right up front to treat philosophical basis immediately,
vis-a-vis something like Mayadayanha and "something? what something?".


Then, a theory of everything kind of neatly works out with a theory of fall gravity
and unifying gravity and the strong nuclear force, in a theory of potentials,
i.e. where the real fields are the potential fields, that is, the fields of potential are
the real fields, and the classical fields are the moments. At least, all the
data of science works better that way.

[Ross Finlayson]

"Es muss sein" and so on.

[olcott]

*In correct reasoning* // *This eliminates the principle of explosion*
A proves B means that B is a semantically necessary consequence of A.

--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer