Page 1 of 1

Search methods

Posted: May 1st, 2018, 4:42 am
by Saka
What are some methods of searching that programs such as zfind and gfind use? LLS is pretty obvious (SAT solver) but what about zfind, gfind, qfind, and WLS?

I ask because I'd like to try making my own search program, perhaps for LTL rules.

Re: Search methods

Posted: May 1st, 2018, 11:48 am
by apg
David Eppstein wrote a paper explaining how gfind works:

https://arxiv.org/abs/cs/0004003

WLS/JLS/lifesrc are similar to LLS, but using an ad hoc solver instead of a commercial SAT solver. Then zfind and ikpx are similar to gfind, but replacing the de Bruijn graph with a large lookup table and an incremental SAT solver, respectively. Finally, qfind is just a parallelised combination of breadth-first and depth-first searching, based on the zfind methodology.