<p>I wrote a simple SAT solver in go. I haven't seen one around yet so I thought it may be interesting for others to share it:</p>
<p><a href="https://github.com/marcvanzee/go-sat">https://github.com/marcvanzee/go-sat</a></p>
<p>The solver can either use a recursive or an iterative algorithm. The algorithm uses a watchlist to keep track of all the assignments (see <a href="http://www-cs-faculty.stanford.edu/%7Euno/programs.html">Knuth's SAT0W program</a>).</p>
<p>Much of the code is based on an <a href="https://github.com/sahands/simple-sat">existing Python implementation</a>. The details of the algorithm, as well as the theoretical background of SAT solving is nicely explained in an <a href="http://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html">accompanying article</a>.</p>
<p>Feel free to give me suggestions on how to improve the code. I learned Go a few weeks ago so it may be very poorly done. I would like to implement some kind of concurrency but this seems quite difficult since the algorithm keeps track of a "watchlist", which should then be copied for every concurrent process.</p>
<hr/>**评论：**<br/><br/>brtzsnr: <pre><p>I also wrote one a long time: <a href="https://bitbucket.org/brtzsnr/gasca/src" rel="nofollow">https://bitbucket.org/brtzsnr/gasca/src</a>. This was based on my master thesis in which I developed a cluster distributed java sat solver.</p></pre>justinisrael: <pre><p>Not sure if you came across this yet, but there is an existing binding for picosat
<a href="https://github.com/wkschwartz/pigosat" rel="nofollow">https://github.com/wkschwartz/pigosat</a></p>
<p>I made a few contributions and have some still pending merge requests. I'm not really experienced with the inner workings of SAT solvers, but I have consumed this API for an application already. </p>
<p>Do you have any examples of using your API?</p></pre>
