Project Overview#

Your research questions will be framed in the context of a new high performance computing system we have implemented for distributing the search performed by decision procedures for the Boolean Satisfiability problem.

For context, examples of such procedures include:

  • the Davis–Putnam–Logemann–Loveland procedure
  • various conflict-driven clause learning procedures.

One of the tasks our system can perform is model counting; I.e., the #SAT problem. Your project will explore the use of distributed model counting to solve probabilistic inference problems exactly.


  • Mathematics or computing students contemplating honours or a PhD.


bars search times arrow-up