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.