Example algorithms
Some examples of algorithms similar to the ones to be used in LarKC are being analysed before the Applied parallelization workshop, July 8th 2008, Amsterdam:
Example code from Cycorp. Michael Witbrock suggests Minisat: http://minisat.se/
SAT is a core inference algorithm for propositional (or, more importantly, propositionalised formulas) that also forms the basis of other inference algorithms (like MLN inference); there's a path of increasing utility from SAT to ?MaxWalkSat to Alchemy that we'll be able to follow (e.g) SAT itself is useful for a bunch of applications (like wire routing on PC boards, and others closer to our immediate needs). A web page about SAT solving is http://www.satlive.org/ .
There is an interesting paper with an overview of the history of SAT solving in the case of propositional logic here:
http://lita.sciences.univ-metz.fr/~singer/SatReview.pdf
Importantly, it also discusses attempts at parallelising certain algorithms (section 4). There is also an interesting description of their own experimentation with parallel evaluation (section 5).
- The DPLL algorithm is discussed at length and a description of this algorithm can be found here:
http://en.wikipedia.org/wiki/DPLL_algorithm
This in turn is based on:
http://en.wikipedia.org/wiki/Davis-Putnam_algorithm
For a description of resolution look here:
http://en.wikipedia.org/wiki/Resolution_%28logic%29
- Finally, an implementation of a scalable, parallelised SAT solver can be found here:
http://ira.informatik.uni-freiburg.de/~schubert/html/miraxt.html