This repository includes an implementation of Shaunak Chatterjee's WalkSATMCMC algorithm from his thesis Efficient inference algorithms for near-deterministic systems, along with some baselines for comparison. WalkSATMCMC is an algorithm aiming to solve near-deterministic probabilistic SAT problems, where each clause represents a high but not deterministic probability of the variables respecting the corresponding constraint, and the goal is to sample from the true joint distribution over the underlying variables. Applying naive MCMC directly to this problem would fail to converge (find the high-probability region) in reasonable time, and though applying WalkSAT directly would provide the variable states with the highest probability (i.e., the solutions to the corresponding deterministic SAT problem), it would fail to capture the fact that the true joint distribution sometimes deviates from these solutions. WalkSATMCMC synthesizes both MCMC and WalkSAT to provide a way to sample in a provably correct way from the joint distribution underlying any near-deterministic probabilistic SAT problems. For more details about the algorithm, please see Shaunak's thesis.
Here are the important files / functions in this repository:
- LogPyMC.py: This script defines a simple probabilistic logic programming language that will be sufficient for defining the probabilistic SAT problems we wish to study
- WalkSATMCMC.py: This script implements WalkSATMCMC, along with two baselines: WalkSATDeterministic (standard WalkSAT) and NaiveSATMCMC (standard MCMC with the proposal distibution involving random single-variable flips)
- experiments/*.py: Two different experiments for comparing the performance of WalkSATMCMC against the baselines.