random sat
31 papers tagged with this keyword
Targeting Clause Type Distributions: a Picklock for Random Satisfiability Problems
Optimization problems such as the NP-complete 3-SAT provide an important benchmark for the difficult task of finding ground-states in strongly correlated many-body systems with rugged energy landscapes. The study of random 3-SAT problems as Ising spin Hamiltonians in statistical physics has yielded major insights including the existence of a satisfiability phase transition, and the prediction of a critical parameter line of particularly hard instances. Yet, progress on solving those instances has been scarce for several decades. Here, introducing the Target-SAT (TSAT) algorithm, we roughly triple the tractable problem sizes in the hardest regime, with an even greater improvement in a vast range of neighboring regions. By leveraging statistical information hidden in the combinatorial constraints of the problem, TSAT is actively guided in its stochastic local search toward a target within the relevant parameter space. Our analysis also explains why established local search algorithms are limited to relatively small system sizes due to a vast low-energy trap. Furthermore, we characterize the aforementioned critical line in terms of a dominant additional complexity barrier, whose exponential scaling is quickly overcome by TSAT only in the surrounding parameter space. With TSAT, the lead in solving the hardest known random satisfiability problems returns to the realm of stochastic local search algorithms.
Inhomogeneous random 2-SAT
We introduce an inhomogeneous variant of random 2-SAT. Each variable $v_1,\ldots,v_n$ is assigned a type from a state space $Λ$, independently at random. Clause inclusion is governed by a symmetric measurable kernel $W$ on $(Λ\times \{+,-\})^2$, in analogy with the inhomogeneous random graph model of Bollobás, Janson, and Riordan: given literals $\ell_i\in\{v_i,\neg v_i\}$ and $\ell_j\in\{v_j,\neg v_j\}$, the clause $\{\ell_i,\ell_j\}$ appears with probability $W(\mathrm{type}(\ell_i),\mathrm{type}(\ell_j))/(2n)$. In particular, for a variable $v_i$ of type $x\inΛ$, the slices $W((+,x),\cdot)$ and $W((-,x),\cdot)$ describe how $v_i$ and $\neg v_i$ interact with other literals.
We identify a parameter $ρ^*(W)$, defined as the spectral radius of an integral operator derived from $W$, and show that $ρ^*(W)<1$ and $ρ^*(W)>1$ correspond to asymptotically almost surely satisfiable and unsatisfiable instances, respectively. The satisfiability threshold for homogeneous random 2-SAT is well-established, occurring when the ratio of clauses to variables is $1$. This corresponds to a weight function of $W \equiv 1$ and a clause density of $1/(2n)$. Our result extends this classical result to a broad class of models controlled by types of variables.
Symmetric Rule-Based Achlioptas Processes for Random $k$-SAT
Inspired by the "power-of-two-choices" model from random graphs, we investigate the possibility of limited choices of online clause choices that could shift the satisfiability threshold in random $k$-SAT.Here, we introduce an assignment symmetric, non-adaptive, topology-oblivious online rule called \emph{MIDDLE-HEAVY}, that prioritizes balanced sign profile clauses.Upon applying a biased $2$-SAT projection and a two-type branching process certificate, we derive closed-form expressions for the shifted thresholds $α_{\textbf{SYM}}(k,\ell)$ for this algorithm.We show that minimal choices $\ell=5$ for $k=4$, $\ell=4$ for $k=5$, and $\ell=3$ for $k\ge 6$ suffice to exceed the asymptotic first-moment upper bound $\sim 2^k \ln 2$ for random $k$-SAT.Moreover, to bridge the gap with biased assignment rules used in maximum of the previous works in this context, we propose a hybrid symmetric biased rule that achieves thresholds comparable to prior work while maintaining symmetry.Our results advance the understanding of Achlioptas processes in random CSPs beyond classical graph-theoretic settings.
On the chromatic number of random triangle-free graphs
We study the chromatic number of typical triangle-free graphs with $Θ\left( n^{3/2} (\log n)^{1/2} \right)$ edges and establish the width of the scaling window for the transitions from $χ= 3$ to $χ= 4$ and from $χ= 4$ to $χ= 5$.
The transition from $3$- to $4$-colorability has scaling window of width $Θ(n^{4/3} (\log n)^{-1/3})$. To prove this, we show a high probability equivalence of the $3$-colorability of a random triangle-free graph at this density and the satisfiability of an instance of bipartite random $2$-SAT, for which we establish the width of the scaling window following the techniques of Bollob{á}s, Borgs, Chayes, Kim, and Wilson.
The transition from $4$- to $5$-colorability has scaling window of width $Θ(n^{3/2} (\log n)^{-1/2})$. To prove this, we show a high probability equivalence of the $4$-colorability of a random triangle-free graph at this density and the simultaneous $2$-colorability of two independent Erdős--Rényi random graphs. For this transition, we also establish the limiting probability of $4$-colorability inside the scaling window.
The random $k$-SAT Gibbs uniqueness threshold revisited
We prove that for any $k\geq3$ for clause/variable ratios up to the Gibbs uniqueness threshold of the corresponding Galton-Watson tree, the number of satisfying assignments of random $k$-SAT formulas is given by the `replica symmetric solution' predicted by physics methods [Monasson, Zecchina: Phys. Rev. Lett. (1996)]. Furthermore, while the Gibbs uniqueness threshold is still not known precisely for any $k\geq3$, we derive new lower bounds on this threshold that improve over prior work [Montanari and Shah: SODA (2007)].The improvement is significant particularly for small $k$.
WalkSAT is linear on random 2-SAT
In an influential article Papadimitriou [FOCS 1991] proved that a local search algorithm called WalkSAT finds a satisfying assignment of a satisfiable 2-CNF with $n$ variables in $O(n^2)$ expected time. Variants of the WalkSAT algorithm have become a mainstay of practical SAT solving (e.g., [Hoos and Stützle 2000]). In the present article we analyse the expected running time of WalkSAT on random 2-SAT instances. Answering a question raised by Alekhnovich and Ben-Sasson [SICOMP 2007], we show that WalkSAT runs in linear expected time for all clause/variable densities up to the random 2-SAT satisfiability threshold.
On the satisfiability of random $3$-SAT formulas with $k$-wise independent clauses
The problem of identifying the satisfiability threshold of random $3$-SAT formulas has received a lot of attention during the last decades and has inspired the study of other threshold phenomena in random combinatorial structures. The classical assumption in this line of research is that, for a given set of $n$ Boolean variables, each clause is drawn uniformly at random among all sets of three literals from these variables, independently from other clauses. Here, we keep the uniform distribution of each clause, but deviate significantly from the independence assumption and consider richer families of probability distributions. For integer parameters $n$, $m$, and $k$, we denote by $\DistFamily_k(n,m)$ the family of probability distributions that produce formulas with $m$ clauses, each selected uniformly at random from all sets of three literals from the $n$ variables, so that the clauses are $k$-wise independent. Our aim is to make general statements about the satisfiability or unsatisfiability of formulas produced by distributions in $\DistFamily_k(n,m)$ for different values of the parameters $n$, $m$, and $k$.
Random $2$-SAT: The set of atoms of the limiting empirical marginal distribution
We show that the set of atoms of the limiting empirical marginal distribution in the random $2$-SAT model is $\mathbb Q \cap (0,1)$, for all clause-to-variable densities up to the satisfiability threshold. While for densities up to $1/2$, the measure is purely discrete, we additionally establish the existence of a nontrivial continuous part for any density in $(1/2, 1)$. Our proof is based on the construction of a random variable with the correct distribution as the the root marginal of a multi-type Galton-Watson tree, along with a subsequent analysis of the resulting almost sure recursion.
The number of random 2-SAT solutions is asymptotically log-normal
We prove that throughout the satisfiable phase, the logarithm of the number of satisfying assignments of a random 2-SAT formula satisfies a central limit theorem. This implies that the log of the number of satisfying assignments exhibits fluctuations of order $\sqrt n$, with $n$ the number of variables. The formula for the variance can be evaluated effectively. By contrast, for numerous other random constraint satisfaction problems the typical fluctuations of the logarithm of the number of solutions are {\em bounded} throughout all or most of the satisfiable regime.
Upper bounds on the $2$-colorability threshold of random $d$-regular $k$-uniform hypergraphs for $k\geq 3$
For a large class of random constraint satisfaction problems (CSP), deep but non-rigorous theory from statistical physics predict the location of the sharp satisfiability transition. The works of Ding, Sly, Sun (2014, 2016) and Coja-Oghlan, Panagiotou (2014) established the satisfiability threshold for random regular $k$-NAE-SAT, random $k$-SAT, and random regular $k$-SAT for large enough $k\geq k_0$ where $k_0$ is a large non-explicit constant. Establishing the same for small values of $k\geq 3$ remains an important open problem in the study of random CSPs.
In this work, we study two closely related models of random CSPs, namely the $2$-coloring on random $d$-regular $k$-uniform hypergraphs and the random $d$-regular $k$-NAE-SAT model. For every $k\geq 3$, we prove that there is an explicit $d_{\ast}(k)$ which gives a satisfiability upper bound for both of the models. Our upper bound $d_{\ast}(k)$ for $k\geq 3$ matches the prediction from statistical physics for the hypergraph $2$-coloring by Dall'Asta, Ramezanpour, Zecchina (2008), thus conjectured to be sharp. Moreover, $d_{\ast}(k)$ coincides with the satisfiability threshold of random regular $k$-NAE-SAT for large enough $k\geq k_0$ by Ding, Sly, Sun (2014).
Polarised random k-SAT
Published
• View Publication
• BIB
In this paper we study a variation of the random $k$-SAT problem, called polarized random $k$-SAT. In this model there is a polarization parameter $p$, and in half of the clauses each variable occurs negated with probability $p$ and pure otherwise, while in the other half the probabilities are interchanged. For $p=1/2$ we get the classical random $k$-SAT model, and at the other extreme we have the fully polarized model where $p=0$, or $1$. Here there are only two types of clauses: clauses where all $k$ variables occur pure, and clauses where all $k$ variables occur negated. That is, for $p=0$ we get an instance of random monotone $k$-SAT. We show that the threshold of satisfiability does not decrease as $p$ moves away from $\frac{1}{2}$ and thus that the satisfiability threshold for polarized random $k$-SAT is an upper bound on the threshold for random $k$-SAT. In fact, we conjecture that asymptotically the two thresholds coincide.
Belief Propagation on the random $k$-SAT model
Published
• View Publication
• BIB
Corroborating a prediction from statistical physics, we prove that the Belief Propagation message passing algorithm approximates the partition function of the random $k$-SAT model well for all clause/variable densities and all inverse temperatures for which a modest absence of long-range correlations condition is satisfied. This condition is known as "replica symmetry" in physics language. From this result we deduce that a replica symmetry breaking phase transition occurs in the random $k$-SAT model at low temperature for clause/variable densities below but close to the satisfiability threshold.
The random 2-SAT partition function
Published
• View Publication
• BIB
We show that throughout the satisfiable phase the normalised number of satisfying assignments of a random $2$-SAT formula converges in probability to an expression predicted by the cavity method from statistical physics. The proof is based on showing that the Belief Propagation algorithm renders the correct marginal probability that a variable is set to `true' under a uniformly random satisfying assignment.
Biased random k-SAT
Published
• View Publication
• BIB
The basic random $k$-SAT problem is: Given a set of $n$ Boolean variables, and $m$ clauses of size $k$ picked uniformly at random from the set of all such clauses on our variables, is the conjunction of these clauses satisfiable?
Here we consider a variation of this problem where there is a bias towards variables occurring positive -- i.e. variables occur negated w.p. $0<p< \frac{1}{2}$ and positive otherwise -- and study how the satisfiability threshold depends on $p$. For $p<\frac{1}{2}$ this model breaks many of the symmetries of the original random $k$-SAT problem, e.g. the distribution of satisfying assignments in the Boolean cube is no longer uniform.
For any fixed $k$, we find the asymptotics of the threshold as $p$ approaches $0$ or $\frac{1}{2}$. The former confirms earlier predictions based on numerical studies and heuristic methods from statistical physics.
The birth of the contradictory component in random 2-SAT
We prove that, with high probability, the contradictory components of a random 2-SAT formula in the subcritical phase of the phase transition have only 3-regular kernels. This follows from the relation between these kernels and the complex component of a random graph in the subcritical phase. This partly settles the question about the structural similarity between the phase transitions in 2-SAT and random graphs. As a byproduct, we describe the technique that allows to obtain a full asymptotic expansion of the satisfiability in the subcritical phase. We also obtain the distribution of the number of contradictory variables and the structure of the spine in the subcritical phase.
Scale-Free Random SAT Instances
Published in Algorithms 15(6): 219 (2022)
• View Publication
• BIB
We focus on the random generation of SAT instances that have properties similar to real-world instances. It is known that many industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide a different generation model of SAT instances, called \emph{scale-free random SAT instances}. It is based on the use of a non-uniform probability distribution $P(i)\sim i^{-β}$ to select variable $i$, where $β$ is a parameter of the model. This results into formulas where the number of occurrences $k$ of variables follows a power-law distribution $P(k)\sim k^{-δ}$ where $δ= 1 + 1/β$. This property has been observed in most real-world SAT instances. For $β=0$, our model extends classical random SAT instances.
We prove the existence of a SAT-UNSAT phase transition phenomenon for scale-free random 2-SAT instances with $β<1/2$ when the clause/variable ratio is $m/n=\frac{1-2β}{(1-β)^2}$. We also prove that scale-free random k-SAT instances are unsatisfiable with high probability when the number of clauses exceeds $ω(n^{(1-β)k})$. %This implies that the SAT/UNSAT phase transition phenomena vanishes when $β>1-1/k$, and formulas are unsatisfiable due to a small core of clauses. The proof of this result suggests that, when $β>1-1/k$, the unsatisfiability of most formulas may be due to small cores of clauses. Finally, we show how this model will allow us to generate random instances similar to industrial instances, of interest for testing purposes.
The number of satisfying assignments of random regular k-SAT formulas
Published
• View Publication
• BIB
Let $Φ$ be a random $k$-SAT formula in which every variable occurs precisely $d$ times positively and $d$ times negatively. Assuming that $k$ is sufficiently large and that $d$ is slightly below the critical degree where the formula becomes unsatisfiable with high probability, we determine the limiting distribution of the logarithm of the number of satisfying assignments.
Walksat stalls well below the satisfiability threshold
Published in SIAM Journal on Discrete Mathematics 31 (2017) 160 - 1173
• View Publication
• BIB
Partly on the basis of heuristic arguments from physics it has been suggested that the performance of certain types of algorithms on random $k$-SAT formulas is linked to phase transitions that affect the geometry of the set of satisfying assignments. But beyond intuition there has been scant rigorous evidence that "practical" algorithms are affected by these phase transitions. In this paper we prove that \walksat, a popular randomised satisfiability algorithm, fails on random $k$-SAT formulas not very far above clause/variable density where the set of satisfying assignments shatters into tiny, well-separated clusters. Specifically, we prove \walksat\ is ineffective with high probability if $m/n>c2^k\ln^2k/k$, where $m$ is the number of clauses, $n$ is the number of variables and $c>0$ is an absolute constant. By comparison, \walksat\ is known to find satisfying assignments in linear time \whp\ if $m/n<c'2^k/k$ for another constant $c'>0$ [Coja-Oghlan and Frieze, SIAM J.\ Computing 2014].
Analysing Survey Propagation Guided Decimation on Random Formulas
Let $\varPhi$ be a uniformly distributed random $k$-SAT formula with $n$ variables and $m$ clauses. For clauses/variables ratio $m/n \leq r_{k\text{-SAT}} \sim 2^k\ln2$ the formula $\varPhi$ is satisfiable with high probability. However, no efficient algorithm is known to provably find a satisfying assignment beyond $m/n \sim 2k \ln(k)/k$ with a non-vanishing probability. Non-rigorous statistical mechanics work on $k$-CNF led to the development of a new efficient "message passing algorithm" called \emph{Survey Propagation Guided Decimation} [Mézard et al., Science 2002]. Experiments conducted for $k=3,4,5$ suggest that the algorithm finds satisfying assignments close to $r_{k\text{-SAT}}$. However, in the present paper we prove that the basic version of Survey Propagation Guided Decimation fails to solve random $k$-SAT formulas efficiently already for $m/n=2^k(1+\varepsilon_k)\ln(k)/k$ with $\lim_{k\to\infty}\varepsilon_k= 0$ almost a factor $k$ below $r_{k\text{-SAT}}$.
The condensation phase transition in random graph coloring
Published in Communication in Mathematical Physics 341 (2016) 543 - 606
• View Publication
• BIB
Based on a non-rigorous formalism called the "cavity method", physicists have put forward intriguing predictions on phase transitions in discrete structures. One of the most remarkable ones is that in problems such as random $k$-SAT or random graph $k$-coloring, very shortly before the threshold for the existence of solutions there occurs another phase transition called "condensation" [Krzakala et al., PNAS 2007]. The existence of this phase transition appears to be intimately related to the difficulty of proving precise results on, e.g., the $k$-colorability threshold as well as to the performance of message passing algorithms. In random graph $k$-coloring, there is a precise conjecture as to the location of the condensation phase transition in terms of a distributional fixed point problem. In this paper we prove this conjecture for $k$ exceeding a certain constant $k_0$.