text: In this work we suggest a new model for generating random satisfiable k-CNF formulas. To generate such formulas -- randomly permute all 2^k n k possible clauses over the variables x_1, ..., x_n, and starting from the empty formula, go over the clauses one by one, including each new clause as you go along if after its addition the formula remains satisfiable. We study the evolution of this process, namely the distribution over formulas obtained after scanning through the first m clauses (in the random permutation's order). Random processes with conditioning on a certain property being respected are widely studied in the context of graph properties. This study was pioneered by Ruci 'nski and Wormald in 1992 for graphs with a fixed degree sequence, and also by Erd o s, Suen, and Winkler in 1995 for triangle-free and bipartite graphs. Since then many other graph properties were studied such as planarity and H-freeness. Thus our model is a natural extension of this approach to the satisfiability setting. Our main contribution is as follows. For m cn, c=c(k) a sufficiently large constant, we are able to characterize the structure of the solution space of a typical formula in this distribution. Specifically, we show that typically all satisfying assignments are essentially clustered in one cluster, and all but e^ - (m n) n of the variables take the same value in all satisfying assignments. We also describe a polynomial time algorithm that finds with high probability a satisfying assignment for such formulas.
  @cite_15: 
  @cite_21: Let G3n,p,3 be a random 3-colorable graph on a set of 3n vertices generated as follows. First, split the vertices arbitrarily into three equal color classes, and then choose every pair of vertices of distinct color classes, randomly and independently, to be edges with probability p. We describe a polynomial-time algorithm that finds a proper 3-coloring of G3n,p,3 with high probability, whenever p @math c n, where c is a sufficiently large absolute constant. This settles a problem of Blum and Spencer, who asked if an algorithm can be designed that works almost surely for p @math polylog(n) n [J. Algorithms, 19 (1995), pp. 204--234]. The algorithm can be extended to produce optimal k-colorings of random k-colorable graphs in a similar model as well as in various related models. Implementation results show that the algorithm performs very well in practice even for moderate values of c.
  @cite_12: We present an algorithm for solving 3SAT instances. Several algorithms have been proved to work whp (with high probability) for various SAT distributions. However, an algorithm that works whp has a drawback. Indeed for typical instances it works well, however for some rare inputs it does not provide a solution at all. Alternatively, one could require that the algorithm always produce a correct answer but perform well on average. Expected polynomial time formalizes this notion. We prove that for some natural distribution on 3CNF formulas, called planted 3SAT, our algorithm has expected polynomial (in fact, almost linear) running time. The planted 3SAT distribution is the set of satisfiable 3CNF formulas generated in the following manner. First, a truth assignment is picked uniformly at random. Then, each clause satisfied by it is included in the formula with probability p. Extending previous work for the planted 3SAT distribution, we present, for the first time for a satisfiable SAT distribution, an expected polynomial time algorithm. Namely, it solves all 3SAT instances, and over the planted distribution (with p = d n2, d > 0 a sufficiently large constant) it runs in expected polynomial time. Our results extend to k-SAT for any constant k.
  @cite_6: Experimental results show that certain message passing algorithms, namely, survey propagation, are very effective in finding satisfying assignments in random satisfiable 3CNF formulas. In this paper we make a modest step towards providing rigorous analysis that proves the effectiveness of message passing algorithms for random 3SAT. We analyze the performance of Warning Propagation, a popular message passing algorithm that is simpler than survey propagation. We show that for 3CNF formulas generated under the planted assignment distribution, running warning propagation in the standard way works when the clause-to-variable ratio is a sufficiently large constant. We are not aware of previous rigorous analysis of message passing algorithms for satisfiability instances, though such analysis was performed for decoding of Low Density Parity Check (LDPC) Codes. We discuss some of the differences between results for the LDPC setting and our results.
summary: Almost all polynomial-time heuristics suggested so far for random instances (either SAT or graph optimization problems) were analyzed when the input is sampled according to a planted-solution distribution, or various semi-random variants thereof. Alon and Kahale @cite_21 suggest a polynomial time algorithm based on spectral techniques that @math properly @math -colors a random graph from the planted @math -coloring distribution (the distribution of graphs generated by partitioning the @math vertices into @math equally-sized color classes, and including every edge connecting two different color classes with probability @math ), for graphs with average degree greater than some constant. In the SAT context, Flaxman's algorithm, drawing on ideas from @cite_21 , solves @math planted 3SAT instances where the clause-variable ratio is greater than some constant. Also @cite_15 @cite_6 @cite_12 address the planted 3SAT distribution.