Random local access for sampling k-SAT solutions

TL;DR

This paper introduces a sublinear time, memory-less algorithm for random local access to uniform solutions of k-SAT formulas at high clause density, enabling efficient sampling of satisfying assignments.

Contribution

It presents the first feasible random local access method for the set of satisfying assignments in k-SAT formulas, combining local uniformity and Glauber dynamics techniques.

Findings

Algorithm operates in sublinear time

Provides memory-less query access to solutions

Works at exponential clause density

Abstract

We present a sublinear time algorithm that gives random local access to the uniform distribution over satisfying assignments to an arbitrary k-SAT formula $\Phi$, at exponential clause density. Our algorithm provides memory-less query access to variable assignments, such that the output variable assignments consistently emulate a single global satisfying assignment whose law is close to the uniform distribution over satisfying assignments to $\Phi$. Random local access and related models have been studied for a wide variety of natural Gibbs distributions and random graphical processes. Here, we establish feasibility of random local access models for one of the most canonical such sample spaces, the set of satisfying assignments to a k-SAT formula. Our algorithm proceeds by leveraging the local uniformity of the uniform distribution over satisfying assignments to $\Phi$. We randomly partition the variables into two subsets, so that each clause has sufficiently many variables from each set to preserve local uniformity. We then sample some variables by simulating a systematic scan Glauber dynamics backward in time, greedily constructing the necessary intermediate steps. We sample the other variables by first conducting a search for a polylogarithmic-sized local component, which we iteratively grow to identify a small subformula from which we can efficiently sample using the appropriate marginal distribution. This two-pronged approach enables us to sample individual variable assignments without constructing a full solution.