-
Witness of unsatisfiability for a random 3-satisfiability formula
Authors:
Lu-Lu Wu,
Hai-Jun Zhou,
Mikko Alava,
Erik Aurell,
Pekka Orponen
Abstract:
The random 3-satisfiability (3-SAT) problem is in the unsatisfiable (UNSAT) phase when the clause density $α$ exceeds a critical value $α_s \approx 4.267$. However, rigorously proving the unsatisfiability of a given large 3-SAT instance is extremely difficult. In this paper we apply the mean-field theory of statistical physics to the unsatisfiability problem, and show that a specific type of UNSAT…
▽ More
The random 3-satisfiability (3-SAT) problem is in the unsatisfiable (UNSAT) phase when the clause density $α$ exceeds a critical value $α_s \approx 4.267$. However, rigorously proving the unsatisfiability of a given large 3-SAT instance is extremely difficult. In this paper we apply the mean-field theory of statistical physics to the unsatisfiability problem, and show that a specific type of UNSAT witnesses (Feige-Kim-Ofek witnesses) can in principle be constructed when the clause density $α> 19$. We then construct Feige-Kim-Ofek witnesses for single 3-SAT instances through a simple random sampling algorithm and a focused local search algorithm. The random sampling algorithm works only when $α$ scales at least linearly with the variable number $N$, but the focused local search algorithm works for clause densty $α> c N^{b}$ with $b \approx 0.59$ and prefactor $c \approx 8$. The exponent $b$ can be further decreased by enlarging the single parameter $S$ of the focused local search algorithm.
△ Less
Submitted 10 March, 2013;
originally announced March 2013.
-
Circumspect descent prevails in solving random constraint satisfaction problems
Authors:
Mikko Alava,
John Ardelius,
Erik Aurell,
Petteri Kaski,
Supriya Krishnamurthy,
Pekka Orponen,
Sakari Seitz
Abstract:
We study the performance of stochastic local search algorithms for random instances of the $K$-satisfiability ($K$-SAT) problem. We introduce a new stochastic local search algorithm, ChainSAT, which moves in the energy landscape of a problem instance by {\em never going upwards} in energy. ChainSAT is a \emph{focused} algorithm in the sense that it considers only variables occurring in unsatisfi…
▽ More
We study the performance of stochastic local search algorithms for random instances of the $K$-satisfiability ($K$-SAT) problem. We introduce a new stochastic local search algorithm, ChainSAT, which moves in the energy landscape of a problem instance by {\em never going upwards} in energy. ChainSAT is a \emph{focused} algorithm in the sense that it considers only variables occurring in unsatisfied clauses. We show by extensive numerical investigations that ChainSAT and other focused algorithms solve large $K$-SAT instances almost surely in linear time, up to high clause-to-variable ratios $α$; for example, for K=4 we observe linear-time performance well beyond the recently postulated clustering and condensation transitions in the solution space. The performance of ChainSAT is a surprise given that by design the algorithm gets trapped into the first local energy minimum it encounters, yet no such minima are encountered. We also study the geometry of the solution space as accessed by stochastic local search algorithms.
△ Less
Submitted 30 November, 2007;
originally announced November 2007.
-
Focused Local Search for Random 3-Satisfiability
Authors:
Sakari Seitz,
Mikko Alava,
Pekka Orponen
Abstract:
A local search algorithm solving an NP-complete optimisation problem can be viewed as a stochastic process moving in an 'energy landscape' towards eventually finding an optimal solution. For the random 3-satisfiability problem, the heuristic of focusing the local moves on the presently unsatisfiedclauses is known to be very effective: the time to solution has been observed to grow only linearly…
▽ More
A local search algorithm solving an NP-complete optimisation problem can be viewed as a stochastic process moving in an 'energy landscape' towards eventually finding an optimal solution. For the random 3-satisfiability problem, the heuristic of focusing the local moves on the presently unsatisfiedclauses is known to be very effective: the time to solution has been observed to grow only linearly in the number of variables, for a given clauses-to-variables ratio $α$ sufficiently far below the critical satisfiability threshold $α_c \approx 4.27$. We present numerical results on the behaviour of three focused local search algorithms for this problem, considering in particular the characteristics of a focused variant of the simple Metropolis dynamics. We estimate the optimal value for the ``temperature'' parameter $η$ for this algorithm, such that its linear-time regime extends as close to $α_c$ as possible. Similar parameter optimisation is performed also for the well-known WalkSAT algorithm and for the less studied, but very well performing Focused Record-to-Record Travel method. We observe that with an appropriate choice of parameters, the linear time regime for each of these algorithms seems to extend well into ratios $α> 4.2$ -- much further than has so far been generally assumed. We discuss the statistics of solution times for the algorithms, relate their performance to the process of ``whitening'', and present some conjectures on the shape of their computational phase diagrams.
△ Less
Submitted 28 January, 2005;
originally announced January 2005.
-
Efficient Algorithms for Sampling and Clustering of Large Nonuniform Networks
Authors:
Pekka Orponen,
Satu Elisa Schaeffer
Abstract:
We propose efficient algorithms for two key tasks in the analysis of large nonuniform networks: uniform node sampling and cluster detection. Our sampling technique is based on augmenting a simple, but slowly mixing uniform MCMC sampler with a regular random walk in order to speed up its convergence; however the combined MCMC chain is then only sampled when it is in its "uniform sampling" mode.Ou…
▽ More
We propose efficient algorithms for two key tasks in the analysis of large nonuniform networks: uniform node sampling and cluster detection. Our sampling technique is based on augmenting a simple, but slowly mixing uniform MCMC sampler with a regular random walk in order to speed up its convergence; however the combined MCMC chain is then only sampled when it is in its "uniform sampling" mode.Our clustering algorithm determines the relevant neighbourhood of a given node u in the network by first estimating the Fiedler vector of a Dirichlet matrix with u fixed at zero potential, and then finding the neighbourhood of u that yields a minimal weighted Cheeger ratio, where the edge weights are determined by differences in the estimated node potentials. Both of our algorithms are based on local computations, i.e. operations on the full adjacency matrix of the network are not used. The algorithms are evaluated experimentally using three types of nonuniform networks: Dorogovtsev-Goltsev-Mendes "pseudofractal graphs", scientific collaboration networks, and randomised "caveman graphs".
△ Less
Submitted 2 June, 2004;
originally announced June 2004.
