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.