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.
Search methods
Search methods
jarring cyan
Re: Search methods
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.
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.
What do you do with ill crystallographers? Take them to the mono-clinic!