Bitstate hashing

<h2 id="use">Use</h2>
<ul><li>Bitstate hashing is utilized in the <a href="/facts/SPIN_model_checker/tFmaY1A2">SPIN</a> model checker for deciding whether a state was already visited by a nested-<a href="/facts/Depth-first_search/luxJKVph">depth-first search</a> algorithm or not. This purportedly led to memory savings of 98% in the case of using one hash function (175 MB to 3 MB) and 92% when two hash functions are used (13 MB). The state coverage dropped to 97% in the former case. <a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a></li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Morris, R. (1968). Scatter Storage Techniques <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Edelkamp, S., & Stein, B. (Eds.). (2004). New Results in Planning, Scheduling, and Design (Puk2004): Workshop; Proceedings. Universität Ulm. <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>Holzmann, G. J. (2003) Addison Wesley. Spin Model Checker, The: Primer and Reference Manual <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
</ol>

Bitstate hashing open-in-new

Bitstate hashing