start on logic/ binary division/ prime finding via DFA constructions

hi all. this continues/ advances the idea of analysis of bertrands postulate via a CS/ automated thm proving approach.

was looking for some existing code around the internet just to see what has been done. years ago, built multiplication circuits in SAT in both C (early 1990s) and Perl (2000s). alas, neither code is still available. (can really tell that you are all on the edge of your seat for that, lol)

there are some interesting papers on fast modulus calculation using highly tuned hardware such as FPGAs. this turned up in a google search pointing to DTIC, Defense Technical Information Center (US military!) and without a citable link on the site, in contrast to many other papers there.[a2][a3][a4]

hmmm!

there are also some nice writeups on binary division on quite a few sites including complement addition approach.[a8][a9][a10][a11]

for this project, was thinking about the modern state of “SMT” (satisfiability modulo theories) which have advanced a lot in the last decade, including standardized libraries etc. (eg “SMT-LIB”/”QF_BV”, standardized bitvector primitives [c2]) and it was interesting, even bordering on fun to poke around and survey developments in this area some.[c] wikipedia has an excellent list of software.[c1] and it was hard to narrow it down because so many systems now support bitvector logic, aka almost “too many to choose from”. found nice implementations/ documentation for CVC[c3][c7], MathSAT[c4][c5], Boolector[c6], Yices[c8], Z3[c9].

but all this seemed overly complicated. these all implement arbitrary integer division by an arbitrary integer, computing quotient and remainder. this project to find prime numbers needs a different logic in the form “find a number such that it doesnt have anything but the trivial factors (1,n)”.

it does not seem to be possible to specify this with a (single) general division circuit and “small” additional constraint(s) on the factor(s). such a construction could find arbitrary composite numbers but not prime numbers. in other words/ in short, it needs to assert the nonexistence of factors, rather than the existence of them.

this is not very “efficient” because for an n-bit number one has to rule out all the Sqrt(n) factors separately. but dont see any other way to do it.

so “in theory” could have utilized a SMT solver but anyway they all seem rather difficult to install, eg requiring unix configure, compile etc and not in binary installable formats (just saw in the chat room a cohort jim struggle with exactly this issue wrt nauty isomorphism detection), and luckily decided, somewhat unexpectedly, dont need the general binary division at all! meantime, do hope that SMT solvers continue to evolve to become more general purpose, easier to install, “less heiroglyphical” etc

(great strides are being taken with SMT technology, its hard to keep up, and even the groundbreaking Konev/ Lisitsa result can be seen as fitting in this area. would really like to see a “highlight reel” for this that crosses fields. some of the SMT solvers have floating point arithmetic and am sure that is a big deal in some applications/ papers, although havent found any on that. SMT seems to be mostly used more in industrial applications (eg electrical engineering/ circuit verification etc) and is not used for cutting edge theorem-proving so much so far, but…

could the day be not far away when a novel SMT proof of a difficult open problem shows up? do expect that myself in the not so distant future… it is the closest to some of my futuristic/ near-outlandish ideas on automated theorem proving etc.; eg one intriguing/ standout ref that captures some similar ideas to SAT induction was from the SPEAR project [c10] which found remarkably performing heuristics/ AI-like approaches to SMT analysis, suggesting major terra incognita yet remains in this area.)

so my next idea is to consider DFA division. this does not seem to be analyzed in a lot of places but did find a few refs on the web.[b] did not find any published papers on the subject (yet) but surely its gotta be in books and papers somewhere. the idea is that DFAs are a nice intermediate step between the problem and pure SAT. (deja vu, this is again exactly as in the much-admirable Konev/ Lisitsa result.)

there is a funky writeup in “geeksforgeeks” using C code, but not very clear.[b2] it turns up in halfway-decent undergrad class course notes at the end [b3] but still not very clear there either.

so then tried to think this thru, and then came up with the basic construction on my lunch hour. the ruby code is so transparent/ clear that am not even going to write out an english description.

this following simple code constructs the binary division by r FSM in the fsmdiv() subroutine followed by a “test harness”. the state numbers correspond to the modulo remainder and initial state is 0. it then picks a random number under 1000 and applies it (“left to right” ie msb to lsb order), and compares the result to standard integer arithmetic and finds it matches. it was called for primes [7,11,13] but it can be called for composites also. the output is the FSM state table, followed by the random number in binary, followed by the transition sequence, and then the verification results line.

fsmdiv.rb

fsmdiv stdout

(4/29) this code is not large but took quite awhile to debug and get all the tiny details right. satdiv generates the SAT formulas for the constant division/ remainder FSM by translating the previously calculated FSMs into SAT, and theres a 2nd piece of code solve that is a rudimentary SAT solver based entirely on unit propagation. the output of the former can be piped into the latter. it uses DIMACS format files.

the stderr output from satdiv is the # of bits in the number to divide “w”, the random number “z”, the random division by one of [7, 11, 13] called “r”, the ruby computed remainder “z % r” and the state machine computed remainder “s”. the other stderr output are the variable assignments in DIMACS format. the generator outputs the “expected” solution and the solver outputs the “actual” solution, which are verified equal as a round-circuit sanity test. following is the stderr output for 3 runs. the 1st w variables represent the random number in binary and the last x variables represent the remainder in binary where x is the number of bits for the divisor r. the intermediate variables are in w groups of x bits to represent the FSM state transitions. the transitions are modelled as a relation between two successive w width groups. the 1st group is “initialized” to state “0”.

satdiv.rb

solve.rb

satdiv | solve stderr

 

a. divide
b. DFA
c. SMT
Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s