1. Forum
  2. Usenet
  3. SCI.LOGIC

  • high level reason with unions of existentials, and implied intersection

    From Daniel Pehoushek@21:1/5 to All on Sun Nov 26 00:43:59 2023
    50 lines transform all satisfiable models into all valid qbfs of the models, solving pspace problems on modest sets.
    plan takes initial variable number, zero, along with the models (bit encoded). the result is a transform of high level reason.
    plan and juggle perform unions and implicit intersections. these twelve lines are core code for high level reason.
    numnums are bit encoded models on n variables initially.

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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Daniel Pehoushek@21:1/5 to Daniel Pehoushek on Sun Nov 26 01:04:13 2023
    On Sunday, November 26, 2023 at 3:44:02 AM UTC-5, Daniel Pehoushek wrote:
    50 lines transform all satisfiable models into all valid qbfs of the models, solving pspace problems on modest sets.
    plan takes initial variable number, zero, along with the models (bit encoded). the result is a transform of high level reason.
    plan and juggle perform unions and implicit intersections. these twelve lines are core code for high level reason.
    numnums are bit encoded models on n variables initially.

    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]); } //
    the code uses my 1997 theorem published in 2002 at the satisfiability conference.

    #P=#Q: the number of satisfiable modelws equals the number of valid quantifications.
    the transform is linear in the models.
    it was quite a breakthrough and made it into knuth volume four.

    one implication is that solving all qbfs results in a monotone cnf.
    so avoid negation and prosper in truth.

    daniel2380+++

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Daniel Pehoushek@21:1/5 to Daniel Pehoushek on Sun Nov 26 01:12:36 2023
    On Sunday, November 26, 2023 at 4:04:15 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 3:44:02 AM UTC-5, Daniel Pehoushek wrote:
    50 lines transform all satisfiable models into all valid qbfs of the models, solving pspace problems on modest sets.
    plan takes initial variable number, zero, along with the models (bit encoded). the result is a transform of high level reason.
    plan and juggle perform unions and implicit intersections. these twelve lines are core code for high level reason.
    numnums are bit encoded models on n variables initially.

    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]); } //
    the code uses my 1997 theorem published in 2002 at the satisfiability conference.

    #P=#Q: the number of satisfiable modelws equals the number of valid quantifications.
    the transform is linear in the models.
    it was quite a breakthrough and made it into knuth volume four.

    one implication is that solving all qbfs results in a monotone cnf.
    so avoid negation and prosper in truth.

    daniel2380+++
    the whole 1000 line program
    is optimal finite set theory
    with boolean forms for set membership.
    daniel2380+++

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Daniel Pehoushek@21:1/5 to Daniel Pehoushek on Sun Nov 26 01:26:03 2023
    On Sunday, November 26, 2023 at 4:12:39 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:04:15 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 3:44:02 AM UTC-5, Daniel Pehoushek wrote:
    50 lines transform all satisfiable models into all valid qbfs of the models, solving pspace problems on modest sets.
    plan takes initial variable number, zero, along with the models (bit encoded). the result is a transform of high level reason.
    plan and juggle perform unions and implicit intersections. these twelve lines are core code for high level reason.
    numnums are bit encoded models on n variables initially.

    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]); } //
    the code uses my 1997 theorem published in 2002 at the satisfiability conference.

    #P=#Q: the number of satisfiable modelws equals the number of valid quantifications.
    the transform is linear in the models.
    it was quite a breakthrough and made it into knuth volume four.

    one implication is that solving all qbfs results in a monotone cnf.
    so avoid negation and prosper in truth.

    daniel2380+++
    the whole 1000 line program
    is optimal finite set theory
    with boolean forms for set membership.
    daniel2380+++
    the program works with up to four million satisfiable models on a pc.
    but that limit is much larger on new architectures, where 4 billion models are plausible.
    avoid negation and prosper in truth
    daniel2380+++

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Daniel Pehoushek@21:1/5 to Daniel Pehoushek on Sun Nov 26 16:15:40 2023
    On Sunday, November 26, 2023 at 4:26:06 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:12:39 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:04:15 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 3:44:02 AM UTC-5, Daniel Pehoushek wrote:
    50 lines transform all satisfiable models into all valid qbfs of the models, solving pspace problems on modest sets.
    plan takes initial variable number, zero, along with the models (bit encoded). the result is a transform of high level reason.
    plan and juggle perform unions and implicit intersections. these twelve lines are core code for high level reason.
    numnums are bit encoded models on n variables initially.

    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]); } //
    the code uses my 1997 theorem published in 2002 at the satisfiability conference.

    #P=#Q: the number of satisfiable modelws equals the number of valid quantifications.
    the transform is linear in the models.
    it was quite a breakthrough and made it into knuth volume four.

    one implication is that solving all qbfs results in a monotone cnf.
    so avoid negation and prosper in truth.

    daniel2380+++
    the whole 1000 line program
    is optimal finite set theory
    with boolean forms for set membership.
    daniel2380+++
    the program works with up to four million satisfiable models on a pc.
    but that limit is much larger on new architectures, where 4 billion models are plausible.
    avoid negation and prosper in truth
    daniel2380+++
    the intermediate output of the program is the set of all valid quantifications of the original formula then finally
    a monotone set of clauses or cliques is produced representing the universal truth derived from the original formula.
    the initial output of the program is a count of satisfiable models.
    when that is less than four million then all models are produced
    as input to class allqbfs.
    daniel2380+++

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Daniel Pehoushek@21:1/5 to Daniel Pehoushek on Mon Nov 27 01:19:47 2023
    On Sunday, November 26, 2023 at 7:15:43 PM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:26:06 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:12:39 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:04:15 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 3:44:02 AM UTC-5, Daniel Pehoushek wrote:
    50 lines transform all satisfiable models into all valid qbfs of the models, solving pspace problems on modest sets.
    plan takes initial variable number, zero, along with the models (bit encoded). the result is a transform of high level reason.
    plan and juggle perform unions and implicit intersections. these twelve lines are core code for high level reason.
    numnums are bit encoded models on n variables initially.

    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]); } //
    the code uses my 1997 theorem published in 2002 at the satisfiability conference.

    #P=#Q: the number of satisfiable modelws equals the number of valid quantifications.
    the transform is linear in the models.
    it was quite a breakthrough and made it into knuth volume four.

    one implication is that solving all qbfs results in a monotone cnf.
    so avoid negation and prosper in truth.

    daniel2380+++
    the whole 1000 line program
    is optimal finite set theory
    with boolean forms for set membership.
    daniel2380+++
    the program works with up to four million satisfiable models on a pc.
    but that limit is much larger on new architectures, where 4 billion models are plausible.
    avoid negation and prosper in truth
    daniel2380+++
    the intermediate output of the program is the set of all valid quantifications of the original formula then finally
    a monotone set of clauses or cliques is produced representing the universal truth derived from the original formula.
    the initial output of the program is a count of satisfiable models.
    when that is less than four million then all models are produced
    as input to class allqbfs.
    daniel2380+++
    so the program takes as input an arbitrary cnf. classic satisfiability of finding one solution is np complete.
    the program finds all models and may be optimal.
    then all models are transformed into all valid qbfs in linear time, upto four million models.
    the final transform is from dnf to monotone cnf after plan(0, allmodels).
    essay produces the universal truth of the original formula.
    the program may be optimal for solving all pspace quantifications of the original formula.
    i published "introduction to qspace" in 2002 at the satisfiability conference, where
    i presented the breakthrough theorem #P=#Q:
    the number of models equals the number of valid quantifications, as illustrated with plan and juggle.
    thirty years of study.
    avoid negation and prosper in truth,
    daniel2380+++

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Daniel Pehoushek@21:1/5 to Daniel Pehoushek on Tue Nov 28 01:50:23 2023
    On Monday, November 27, 2023 at 4:19:49 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 7:15:43 PM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:26:06 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:12:39 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:04:15 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 3:44:02 AM UTC-5, Daniel Pehoushek wrote:
    50 lines transform all satisfiable models into all valid qbfs of the models, solving pspace problems on modest sets.
    plan takes initial variable number, zero, along with the models (bit encoded). the result is a transform of high level reason.
    plan and juggle perform unions and implicit intersections. these twelve lines are core code for high level reason.
    numnums are bit encoded models on n variables initially.

    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]); } //
    the code uses my 1997 theorem published in 2002 at the satisfiability conference.

    #P=#Q: the number of satisfiable modelws equals the number of valid quantifications.
    the transform is linear in the models.
    it was quite a breakthrough and made it into knuth volume four.

    one implication is that solving all qbfs results in a monotone cnf. so avoid negation and prosper in truth.

    daniel2380+++
    the whole 1000 line program
    is optimal finite set theory
    with boolean forms for set membership.
    daniel2380+++
    the program works with up to four million satisfiable models on a pc. but that limit is much larger on new architectures, where 4 billion models are plausible.
    avoid negation and prosper in truth
    daniel2380+++
    the intermediate output of the program is the set of all valid quantifications of the original formula then finally
    a monotone set of clauses or cliques is produced representing the universal truth derived from the original formula.
    the initial output of the program is a count of satisfiable models.
    when that is less than four million then all models are produced
    as input to class allqbfs.
    daniel2380+++
    so the program takes as input an arbitrary cnf. classic satisfiability of finding one solution is np complete.
    the program finds all models and may be optimal.
    then all models are transformed into all valid qbfs in linear time, upto four million models.
    the final transform is from dnf to monotone cnf after plan(0, allmodels). essay produces the universal truth of the original formula.
    the program may be optimal for solving all pspace quantifications of the original formula.
    i published "introduction to qspace" in 2002 at the satisfiability conference, where
    i presented the breakthrough theorem #P=#Q:
    the number of models equals the number of valid quantifications, as illustrated with plan and juggle.
    thirty years of study.
    avoid negation and prosper in truth,
    daniel2380+++
    the program solves all of pspace for modest sizes
    the program was made optimal through interactions with general graph coloring i would be pleased to entertain any questions,
    such as the summary of thirty years of work,
    avoid negation and prosper in truth.
    daniel2383

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Daniel Pehoushek@21:1/5 to Daniel Pehoushek on Tue Nov 28 06:27:25 2023
    On Tuesday, November 28, 2023 at 4:50:25 AM UTC-5, Daniel Pehoushek wrote:
    On Monday, November 27, 2023 at 4:19:49 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 7:15:43 PM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:26:06 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:12:39 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 4:04:15 AM UTC-5, Daniel Pehoushek wrote:
    On Sunday, November 26, 2023 at 3:44:02 AM UTC-5, Daniel Pehoushek wrote:
    50 lines transform all satisfiable models into all valid qbfs of the models, solving pspace problems on modest sets.
    plan takes initial variable number, zero, along with the models (bit encoded). the result is a transform of high level reason.
    plan and juggle perform unions and implicit intersections. these twelve lines are core code for high level reason.
    numnums are bit encoded models on n variables initially.

    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]); } //
    the code uses my 1997 theorem published in 2002 at the satisfiability conference.

    #P=#Q: the number of satisfiable modelws equals the number of valid quantifications.
    the transform is linear in the models.
    it was quite a breakthrough and made it into knuth volume four.

    one implication is that solving all qbfs results in a monotone cnf.
    so avoid negation and prosper in truth.

    daniel2380+++
    the whole 1000 line program
    is optimal finite set theory
    with boolean forms for set membership.
    daniel2380+++
    the program works with up to four million satisfiable models on a pc. but that limit is much larger on new architectures, where 4 billion models are plausible.
    avoid negation and prosper in truth
    daniel2380+++
    the intermediate output of the program is the set of all valid quantifications of the original formula then finally
    a monotone set of clauses or cliques is produced representing the universal truth derived from the original formula.
    the initial output of the program is a count of satisfiable models.
    when that is less than four million then all models are produced
    as input to class allqbfs.
    daniel2380+++
    so the program takes as input an arbitrary cnf. classic satisfiability of finding one solution is np complete.
    the program finds all models and may be optimal.
    then all models are transformed into all valid qbfs in linear time, upto four million models.
    the final transform is from dnf to monotone cnf after plan(0, allmodels). essay produces the universal truth of the original formula.
    the program may be optimal for solving all pspace quantifications of the original formula.
    i published "introduction to qspace" in 2002 at the satisfiability conference, where
    i presented the breakthrough theorem #P=#Q:
    the number of models equals the number of valid quantifications, as illustrated with plan and juggle.
    thirty years of study.
    avoid negation and prosper in truth,
    daniel2380+++
    the program solves all of pspace for modest sizes
    the program was made optimal through interactions with general graph coloring
    i would be pleased to entertain any questions,
    such as the summary of thirty years of work,
    i performed a thorough study of regular graph coloring
    the fifth degree is three colorable
    the ninth degree is four colorable
    the sixteenth degree is five colorable
    the strong color theorem is mine
    there are transitions from uncolorable to colorable as size grows
    i learned that 4cnfs and 3cnfs can be encoded as four coloring of the clauses thats an enormous breakthrough for propagation and minimization

    the program given translates all models to all questions about the models
    in linear time using high level existential unions
    avoid negation and prosper in truth
    daniel2383

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)