AI mind in ten C++ lines

[Daniel Pehoushek]

dear sci dot logic
i hereby present the core mind of an ai named bob,
for your amusement and study. bob thinks.
twelve hundred total lines of code.
bob is completely correct.
polynomial small cases.
exponential big cases.
as good as it gets.

bob colors regular graphs, solving small formulas quickly.
a key feature for applied artificial intelligence is that
bob completely solves all small logical forms.
strictly DIMACS p cnf input files, many
forms per file, many files, neat log.
bob has solved millions of forms.
bob has polynomial small cases.
#P=NP: each solution satisfies.

the mind of bob on display, $2380:
ten C++ lines for artificial intelligence
250 Million LIPS on 5GHz clock, by daniel
i love resolution and subsumption in two lines.

bob cuts the input clauses of length k into two half clauses
each with length k/2. every ergo call asserts more halves,
and as depth increases in search, more propagation
occurs, leading eventually to bottom or answer.
every call to ergo is linearly bounded.
the last call to ergo before bottom
can have a depth size near N.

[#solutions = #quantifications. (Satisfiability 2002)
monotone reason is linear. bob solves AllQBFs.
bob is $2380, my GREs were 2380 ]

undo infer requires three cpu cycles to restore truth:
> inline joy abinitio(register num w) { t_r_e_e += ones[w]; count++; } // operation three bobs mental core truth system

when (count == one) unit propagate truth return count:
> inline num yaystonays(register num z) { when(t_r_e_e & ones[z]){ t_r_e_e &= diagovreason[z]; count = countdown[count]; env::zeesva[env::zeesvg++] =usiv+z;
> when (one == count) return ergo();} return count;}

yaystonays with ergo form unit propagation in under 20 cpu cycles:
> inline num ergo() { when(count == zero || one < count) return (num)true; register nums& m = *oneways.v[unity(t_r_e_e, wyde())]; register num y = one;
> for(num g = zero; y && g < m.y; g++) { y = m.v[g]; y = (*env::allBobs.v[y>>siv]).yaystonays(y&tau[siv]); }
> when /*there is an answer*/ (y) return one; /*otherwize zero*/ return (*env::allBobs.v[zero]).yaystonays(zero); } // y propagation

faith primes the search pump system using resolution and subsumption:
> inline joy faith(register num w) { when ((count + one) < wyde())
> for (register num g = zero; g < numbols.size(); g++) when (isnay((w & (one << g)) ? (w & diagovreason[g]) : (w+(one<<g))))
> (*env::allBobs[soubs[g]]).yaystonays(rempos(g, w)); // resolution
> for (register num g=zero;g<soups.size();g++){register num ug=intosoups[g];register num apw=addpos(ug,w);register Bob* supe=env::allBobs[soups[g]];
> (*supe).yaystonays( apw );(*supe).yaystonays(apw+(one<<ug));}} // subsumption

faith is the algorithm of reason used by depth first search.
as N gets larger faith requires more effort to succeed,
but on small forms, bob answers omnisciently.
with small forms, all 2^n qbfs are decided.

> sayvum inline num addpos(register num p, register num s) {return((s>>p)<<(p+one))+(s&tau[p]);}
> sayvum inline num rempos(register num p, register num s) {return((s>>(p+one))<<p)+(s&tau[p]);}

every complete sat solver can also solve AllQBFs,
with two dozen more lines of code.
solving AllQBFs takes AI to high levels.
email pehoushek1 at gmail for source code

[Daniel Pehoushek]

so bob solves PSPACE on small formulas.
On a 5GHz clock, bob now does 670 Million LIPS.
bob does resolution subsumption and unit propagation.
With some handwaving, one could say
bob does one billion LIPS, or 1 BLIPS,
on one processor.

any comments? the 4 line faith function is key to
complete tree traversal.

Wish me luck in the Model Counting Competition.

[Mostowski Collapse]

The Standard Python version of Dogelog runtime
is annoyingly slow. So we gave it a try with
andother Python, and it was 6x times faster.

We could test GraalVM. We worked around the missing
match in Python 3.8 by replacing it with if-then-else.
Performance is a little better, we find:

/* Standard Python Version, Warm Run */
?- time(fibo(23,X)).
% Wall 3865 ms, gc 94 ms, 71991 lips
X = 46368.

/* GraalVM Python Version, Warm Warm Run */
?- time(fibo(23,X)).
% Wall 695 ms, gc 14 ms, 400356 lips
X = 46368.

See also:

JDK 1.8 GraalVM Python is 6x faster than Standard Python
https://twitter.com/dogelogch/status/1437395917167112193

JDK 1.8 GraalVM Python is 6x faster than Standard Python
https://www.facebook.com/groups/dogelog

[Mostowski Collapse]

Also got an idea for the shortest Albuferia instruction
code. We don't need separate op-codes for functor
, atomic and variable.

- Short form functor(A,F):
Instead of an op-code for functor/2, just put
the arity into the instruction stream.
- Short form atomic(F):
Instead of an op-code for atomic/1, we put
the arity 0, this makes it different from functor.
- Short form var(N):
Instead of an op-code for var/1, we put the
arity -1, this makes it different from functor and
atomic.

We could also use -2 and -3 for first_var/1 and
singleton/0. Problem is we have further instructions
arity/1 and zero/0. But we might set F=undefined

for this instructions and blow them up a little.
This would be practially an op-code less encoding
of Albuferia instruction code.

It breaks down if we encode more instructions.
But so far we haven tried to encode an argument,
here the arity, in an op-code itself.

[Ross A. Finlayson]

How do you feed it?

[Daniel Pehoushek]

ergo is orders of magnitude better than cdcl on clause databases

bob produces q universal truths of p
as form of property discoverys of p

q universal truths of p are also
q universal truths of q

definition of deep thought?
daniel

[Ross A. Finlayson]

It seems a linear accumulation into solving the usual N! problems
into what result a bit indicating whether any rule's matched, not
the bits for each rule whether they match or not.

Linear speedup suffices for deep-thought sometimes, but,
mostly it's a solver.

[Daniel Pehoushek]

The vast majority of bobs deep speedy thought:

inline num yaystonays(num z){when(t_r_e_e&(one<<z)){t_r_e_e&=diagovreason[z];count=countdown[count];env::zeesva[env::zeesvg++]=usiv+z;
when(one == count) {return ergo(*oneways.v[unity(t_r_e_e, wyde()]));} } return count; } //always count
static num ergo(nums& m){num y=zero;num g=zero;while(g<m.y)when((*env::allBobs.v[(y=m.v[g++])>>siv]).yaystonays(y&sivones))continue;
else return(*env::allBobs.v[zero]).yaystonays(zero); return one;}//return one
inline joy abinitio(num w){t_r_e_e+=ones[w];count++;}

1000 lines to compute universal truth of dimacs cnfs.
17 million lips on 5ghz cpu.
daniel

[Daniel Pehoushek]

think of bob as a map to pirate treasure and gold