Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- #P=#Q number of solutions equals number of quantificates, then what?
- dear benchmarks at mccompetition dot org,
- so you count all satisfying solutions. then what?
- so, here is bob, for making qformulas out of all solutions,
- for correctly deciding all 2^n qbfs. but first,
- i briefly sketch two prior results, sublinear patterns,
- plus nlogn +vision. then, complete leftright sorting of sets,
- with ezistentialism on the left, universalism on the right.
- a linear transform from all solutions to all quantificates.
- the bobbyfish code may be easily added to any complete solver.
- on my computer, the practical finite limit is ten million
- quantificates per formula.
- +++ skip
- optimal string matching, O(N/M) on all alphabets, including size two alphabets.
- M is number of pattern letters. logM is key size where log base is A, the alphabet size.
- preprocessing time O(MlogM) over all parts, followed by partitioning text size N by
- Precisely(one + M -logM), comparing keys of text with keys of pattern, in time O(N/M logM).
- ignoring logs, string matching is thus O(m + n/m), or, O(n/m). (CPM98)
- sublinear algorithms may be the essence of digestion.
- +++ +vision
- cardiff software had an industrial nlogn +vision system on n pizels.
- find two empty lines, forming a plus, then call +vision four times.
- animals do leftright set sorting using vision plus patterns. so.
- +++ bobbyfish
- given a set of satisfying solutions, bob is a linear leftright
- set sorting algorithm for solving all 2^n qbfs. linear.
- please observe, the exciting theme that the number N of
- boolean variables is missing from bobbyfish.
- further research is clearly necessary.
- the biggest money is in the smallest formulas, often just
- logm boolean variables of some partial mental pattern.
- typedef unsigned long num;
- num diagonalofreason[] = { /*thirtytwo valuable zeroes ninehundredninetytwo agreeable ones */
- /* #P=#Q number satisfying solutions equals number valid quantifications (Satisfiability 2002) */
- (num)4294967294, (num)4294967293, (num)4294967291, (num)4294967287,/*my favorite set of four numbers in base ten*/
- (num)4294967279, (num)4294967263, (num)4294967231, (num)4294967167, /* called workhorse+of+reason by daniel */
- (num)4294967039, (num)4294966783, (num)4294966271, (num)4294965247, /* constants of reason have names */
- (num)4294963199, (num)4294959103, (num)4294950911, (num)4294934527, /* ultimate answers are finite */
- (num)4294901759, (num)4294836223, (num)4294705151, (num)4294443007, /* gods favorite number is three */
- (num)4293918719, (num)4292870143, (num)4290772991, (num)4286578687, /* bobs favorite number is five */
- (num)4278190079, (num)4261412863, (num)4227858431, (num)4160749567, /* my favorite nunber is ten */
- (num)4026531839, (num)3758096383, (num)3221225471, (num)2147483647 /* +vision is nlogn skip is n/m */};
- const num one = (num)true; /// first principle in the beginning one
- const num zero = one >> one; /// zero by one down one
- const num two = one + one + zero; /// second principle
- const num three = two + one; /// there /// main result of my lifes work
- const num seven = three + three + one; /// favorite number of many
- const num thirtyone = seven + seven + three + seven + seven; /// my favorite birthdate construction
- num tautologies[]={/* spelled out */zero, one, three, seven, seven+seven+one, thirtyone, thirtyone+one+thirtyone,/* compiled tauts in base ten */ 127, 255, 511, 1023, 2047, 4095, 8191, 16383, 32767, 65535 };
- const num five = tautologies[tautologies[one] << tautologies[one]] + tautologies[one] << tautologies[one]; // bobs number may be alephnull of reason
- const num thefifthtautology = tautologies[five]; // bobs only high order tautology for solving all qbfs without reference of N
- class bobbyfish { // converts tree of satisfying assignments into tree of valid quantifications
- public: // fortytwo: what is fiftyfour in base thirteen representation? perhaps postulated number of triilliverses.
- static num be /*is bit on*/ (nums& s, num b) { return (s[ b >> five ] & (one << (b & thefifthtautology )));}
- static void spread /*leftright around bit*/ (num b, numnums& s, numnums& l, numnums& r) { for (num g = zero; g < s.size(); g++) if (be( (*s[g]), b )) r.add(s[g]); else l.add(s[g]); }
- static void goldytuboody /*if on turn bit off*/ (nums& s, num b) { if (be(s,b)) s[b >> five] &= diagonalofreason[b & thefifthtautology ]; else; }
- static void qtree /* */ (num v, numnums& s) { if (zero == s.size()) return; numnums l; numnums r; spread (v, s, l, r); s.setsize(zero);
- qtree (v + one, l); qtree (v + one, r); utree (v, l, r); // leftright sortset
- for (num g = zero; g < l.size (); g++) { oldybutgoody (*(l[g]), v); s.add (l[g]); } l.setsize(zero);
- for (num g = zero; g < r.size (); g++) { s.add (r[g]); } r.setsize(zero); }
- static void utree /*33*/ (num v, numnums& l, numnums& r)
- { if (zero == l.size()) { for (num g = zero; g < r.size(); g++) l.add(r[g]); r.setsize(zero); return; }
- numnums al; numnums ar; spread (v + one, l, al, ar); l.setsize (zero);
- numnums bl; numnums br; spread (v + one, r, bl, br); r.setsize(zero);
- utree (v + one, al, bl); utree (v + one, ar, br);
- for (num g = zero; g < al.size(); g++) { l.add (al[g]); } al.setsize(zero);
- for (num g = zero; g < ar.size(); g++) { l.add (ar[g]); } ar.setsize(zero);
- for (num g = zero; g < bl.size(); g++) { r.add (bl[g]); } bl.setsize(zero);
- for (num g = zero; g < br.size(); g++) { r.add (br[g]); } br.setsize(zero); }
- static numnums solutions; // the finite set of all satisfying solutions
- static void addsolution() { /* system dependent */ return solutions.size(); }
- static void bob(){qtree(zero,solutions);} //qtransform back into solutions
- };
- about thirty line decomposition, i have yet to write ((see bachus 2009...)).
- bob.cpp is available, two thousand lines, twenty year old file.
- bobs training datasets are all small graph coloring formulas in dimacs form.
- argg.cpp, a regular graph generator is available.
- my two best data sets are c4d9n200s and c3d5n180s.
- 200 four day formulas, and 32,400 one minute formulas,
- 400 and 360 variables respectively, great for benchmarks
- and correctness comparisons among systems.
- there are even thirtyfive unsatisfiables.
- bob has solved two million formulas in one run.
- my best minus ever is in this email. just try deleting that, for
- good but not quite right results. there is one minus in bob.cpp,
- a monotone program, for reading dimacs benchmarks. personally,
- i prefer ~ or + as the letter indicating that the proposition
- should be twiddled for reason. i do not believe in negation.
- (sincerely daniel (little d)) gres 2380 800v 800m 780a
- ps please, someone, reply, to prove, to me, that,
- your email addess, is, a nonempty, bitbuckit.
- mine is pehoushek1 at gmail dot com
- pps in years past i have completely failed
- in my attempts to contact academia.
- i thought my gres certificate
- had very high quality, but,
- null responses from
- hundreds of attempts
- was the main result
- that i have never
- fully understood.
- seven sigmas
- are so rare.
- so this time i include my mailing list
- inside the attached file of the email.
- i try every few years nowadays...
- the list is several years old.
- benchmarks@mccompetition.org and to ruediger and johannes
- ==============================================================================================================================================
- to ::::::::::
- christos@cs.berkeley.edu dek@cs.stanford.edu phw@csail.mit.edu pratt@cs.stanford.edu franco@gauss.ececs.uc.edu
- ret@cs.princeton.edu shanghua@usc.edu jchayes@microsoft.com matias@google.com avg@soe.ucsc.edu
- rwilliams@gmail.com bayardo@alum.mit.edu jtropp@cms.caltech.edu plaisted@cs.unc.edu moses@cs.stanford.edu
- reingold@stanford.edu tim@cs.stanford.edu ullman@gmail.com valiant@stanford.edu ronitt@csail.mit.edu
- genesereth@stanford.edu shoham@stanford.edu virgi@cs.stanford.edu aaronson@cs.utexas.edu shor@math.mit.edu
- danama@cs.utexas.edu shafi@csail.mit.edu karger@mit.edu jehkim@microsoft.com dana.randall@cs.gatech.edu
- kolaitus@us.ibm.com fagin@us.ibm.com vitaly.edu@gmail.com kclarks@us.ibm.com konak@us.ibm.com
- megiddo@us.ibm.com froberts@dimacs.rutgers.edu madhu@cs.harvard.edu Giunchiglia@unige.it
- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
- jkatz@cs.umd.edu gasarch@cs.umd.edu plaxton@cs.utexas.edu russell@cs.ucsd.edu
- omer@cs.ucsb.edu rs@cs.princeton.edu eva.tardos@cornell.edu jeh@cs.cornell.edu
- schwartz@cs.fsu.edu fan@ucsd.edu gnf@cs.purdue.edu kal4@case.edu
- beame@cs.washington.edu glencora@eecs.oregonstate.edu darwiche@cs.ucla.edu jeffe@illinois.edu
- chen@cse.nd.edu SxR48@psu.edu sidiropoulos.1@osu.edu sleator@cs.cmu.edu
- rudich@cs.cmu.edu odonnell@cs.cmu.edu haeupler@cs.cmu.edu yann@cs.nyu.edu
- yann@fb.com
- jyc@cs.wisc.edu dieter@cs.wisc.edu chengb@cse.msu.edu allison@cs.columbia.edu
- csxichen@gmail.com rocco@cs.columbia.edu cliff@ieor.columbia.edu mihalis@cs.columbia.edu
- lane@cs.rochester.edu debmalya@cs.duke.edu barring@cs.umass.edu immerman@cs.umass.edu
- klein@cs.brown.edu ram@cs.stonybrook.edu skiena@cs.sunysb.edu kundu@csc.lsu.edu
- evw@cs.umn.edu eppstein@ics.uci.edu dan@ics.uci.edu lueker@ics.uci.edu
- chen@cse.tamu.edu razborov@cs.uchicago.edu milos@cs.pitt.edu chitta@asu.edu
- joolee@asu.edu atri@buffalo.edu xinhe@buffalo.edu choueiry@cse.unl.edu byc@acm.org
- Joan.Feigenbaum@yale.edu james.aspnes@gmail.com spielman@cs.yale.edu pwp@cs.indiana.edu
- dughof@indiana.edu Khot@cs.nyu.edu regehr@cs.utah.edu zvonimir@cs.utah.edu
- kirby@cs.utah.edu allender@cs.rutgers.edu swastik@math.rutgers.edu szegedy@cs.rutgers.edu
- saks@math.rutgers.edu fperezcr@stevens.edu glencora@eecs.orst.edu cwilson@cs.uoregon.edu
- xiaodiwu@cs.uoregon.edu
- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
- sat committee
- sergeg@cse.unsw.edu.au Leberre@cril.fr weaversa@gmail.com marijn@cs.utexas.edu uwe@kr.tuwien.ac.at
- carsten.sinz@gmail.com lsimon@labri.fr matti.jarvisalo@cs.helsinki.fi jakobn@kth.se oliveras@cs.upc.edu
- Olivier.roussel@cril.univ-artois.fr fbacchus@cs.toronto.edu sbuss@ucsd.edu hoos@cs.ubc.ca
- paturi@cs.ucsd.edu Jussi.Rintanen@aalto.fi roberto.sebastiani@unitn.it selman@cs.cornell.edu sz@ac.tuwien.ac.at
- tamura@kobe-u.ac.jp tw@cse.unsw.edu.au ofers@ie.technion.ac.il O.Kullmann@Swansea.ac.uk karem@umich.edu
- sat 2017 authors et cetera
- e.freuder@4c.ucc.ie bessiere@lirmm.fr larsko@cs.ubc.ca Mark.Wallace@monash.edu
- agostino.dovier@uniud.it narodytska@gmail.com epontell@nmsu.edu
- mitchell@cs.sfu.ca pocr@pragmaticsofsat.org Philippe.Codognet@lip6.fr daniel.diaz@univ-paris1.fr
- organizers@satcompetition.org qbf17@qbflib.org optas@cs.ucsc.edu audemard@cril.fr
- O.Beyersdorff@leeds.ac.uk jcb@mie.utoronto.ca bart.bogaerts@cs.kuleuven.be
- rganian@ac.tuwien.ac.at grigory@cs.washington.edu aaknop@gmail.com dmitrits@pdmi.ras.ru
- strejcek@fi.muni.cz lammich@in.tum.de jakobn@kth.se vinyals@kth.se inoue@nii.ac.jp
- vganesh@uwaterloo.ca ppoupart@uwaterloo.ca fslivovsky@ac.tuwien.ac.at peitl@ac.tuwien.ac.at
Add Comment
Please, Sign In to add comment
