## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Unsatisfiable random formulas are hard to certify

LICS, pp.325-334, (2002)

EI WOS

Abstract

We prove that every property of 3CNF formulas that implies unsatisfiability and is expressible in Datalog has asymptotic probability zero when formulas are randomly generated by taking 6n non-trivial clauses of exactly three literals uniformly and independently. Our result is a consequence of designing a winning strategy for Duplicator in...More

Code:

Data:

Introduction

- The design of the winning strategy for Duplicator relies on the fact that the incidence graph of a random 3CNF formula, the bipartite graph that relates clauses with the variables that occur in them, satisfies certain extension axioms that the authors introduce based on the expander properties of the graph.
- An immediate corollary of the main result about Duplicator winning the n=(ln n)2-pebble game on a random 3CNF formula F , and the size-width trade-off of [BSW01], is that every Resolution refutation of F requires size 2 (n=(ln n)[4]).

Highlights

- The so-called phase transition that certain combinatorial problems exhibit has inspired an alternative line of research within the field of Computational Complexity
- It turns out that the probability that such a random formula F is satisfiable exhibits a sharp threshold around a critical c 4:2
- Experimental results suggest that c is around 4:2 [SML96], but the existence of such a constant is only a conjecture for the moment [CR92]. This structural analysis of the typical instance of the 3CNF satisfiability problem is complemented by an analysis of the average-case computational complexity of solving it
- The design of the winning strategy for Duplicator relies on the fact that the incidence graph of a random 3CNF formula, the bipartite graph that relates clauses with the variables that occur in them, satisfies certain extension axioms that we introduce based on the expander properties of the graph
- We show the existence of a Datalog program P with 2k variables such that (1) if F has a Resolution refutation of width k, P evaluates true on the structure encoding F, and (2) if P evaluates true on the structure encoding F, F has a Resolution refutation of width 2k
- An immediate corollary of the proof of Theorem 5 and Theorem 8 is that every Resolution refutation of a a random 3CNF formula requires width n=2(ln n)[2] with probability approaching 1

Results

- The result that the authors obtain is that if G is an (s; )-bipartite expander of left-degree at most l, Disprover wins the matching game with r s=(l + ) fingers.
- Note for the record that Duplicator is answering consistently with the partial truth assignment corresponding to t+1 and Vt+1, the partial matching and the set of pebbled variables in the existential r0-pebble game at time t + 1.
- She will need to do some bookeeping in the matching game: Let D = fC1; : : : ; Clg be the set of clauses of F on which variable x occurs.
- When Spoiler puts a new pebble, Duplicator answers according to the partial truth assignment corresponding to the partial matching t+1 and the set of pebbled variables Vt+1, and this cannot tu falsify a clause from F by Lemma 3.
- She will keep track of a partial matching t in the complete bipartite graph Knn+1 with the following property: Pigeon i 2 f1; : : : ; n + 1g belongs to Dom( t) if and only if some variable of pigeon i is pebbled at the end of round t.
- Let them consider the possible moves of Spoiler at time t + 1 separately: If Spoiler places a pebble over a variable pi;j, Duplicator acts as follows: If i 2 Dom( t), Duplicator answers 1 if j = t(i) and 0 otherwise.
- This is expressed by the conjunction of the following set of clauses on the variables fxe : e 2 Eg. For every u 2 U, let

Conclusion

- Theorem 8 There exists a 2k-Datalog sentence ' such that for every 3CNF formula F , the following holds: (i) If F has a Resolution refutation of width k, M(F ) j= '.
- An immediate corollary of the proof of Theorem 5 and Theorem 8 is that every Resolution refutation of a a random 3CNF formula requires width n=2(ln n)[2] with probability approaching 1

Reference

- A. Atserias, M. L. Bonet, and J. L. Esteban. Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. Accepted for publication in Information and Computation. A preliminary version appeared in ICALP’01, Lecture Notes in Computer Science 2076, Springer, pages 1005–1016., 2001.
- [Ach01] D. Achlioptas. A survey of lower bounds for random 3-SAT via differential equations. Theoretical Computer Science, 265(1–2):159–185, 2001.
- [AS00] D. Achlioptas and G.B. Sorkin. Optimal myopic algorithms for random 3-SAT. In 41st Annual IEEE Symposium on Foundations of Computer Science, pages 590–600, 2000.
- [BFU93] A. Z. Broder, A. M. Frieze, and E. Upfal. On the satisfiability and maximum satisfiability or random 3-CNF formulas. In 4th Annual ACM-SIAM Symposium on Discrete Algorithms, pages 322–330, 1993.
- [BH79] A. Blass and F. Harary. Properties of almost all graphs and complexes. Journal of Graph Theory, 3:225–240, 1979.
- [BKPS99] P. Beame, R. Karp, T. Pitassi, and M. Saks. The efficiency of resolution and DavisPutnam procedures. Submitted; final version of FOCS’96 and STOC’98, 1999.
- [BSG01] E. Ben-Sasson and N. Galesi. Space complexity of random formulas in resolution. In 16th IEEE Conference in Computational Complexity, 2001.
- [BSI99] E. Ben-Sasson and R. Impagliazzo. Random CNF’s are hard for the polynomial calculus. In 40th Annual IEEE Symposium on Foundations of Computer Science, 1999.
- [BSW01] E. Ben-Sasson and A. Wigderson. Short proofs are narrow–resolution made simple. Journal of the ACM, 48(2):149–169, 2001.
- [CR79] S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44:36–50, 1979.
- [CR92] V. Chvatal and B. Reed. Mick gets some (the odds are on his side). In 33rd Annual IEEE Symposium on Foundations of Computer Science, pages 620–627, 1992.
- [CS88] V. Chvatal and E. Szemeredi. Many hard examples for resolution. Journal of the ACM, 35(4):759–768, 1988.
- [Fag76] R. Fagin. Probabilities on finite models. Journal of Symbolic Logic, 41:50–58, 1976.
- [Hak85] A. Haken. The intractability of resolution. Theoretical Computer Science, 39:297–308, 1985.
- [JSV00] S. Janson, Y. C. Stamatiou, and M. Vamvakari. Bounding the undatisfiability threshold of random 3-SAT. Random Structures and Algorithms, 17(2):103–116, 2000.
- [KV90] Ph. G. Kolaitis and M. Y. Vardi. 0-1 laws and decision problems for fragments of second-order logic. Information and Computation, 87:302–338, 1990.
- [KV95] Ph. G. Kolaitis and M. Y. Vardi. On the expressive power of Datalog: tools and a case study. Journal of Computer and System Sciences, 51:110–134, 1995.
- [KV00] Ph. G. Kolaitis and M. Y. Vardi. Conjunctive-query containment and constraint satisfaction. Journal of Computer and System Sciences, 61(2):302–332, 2000.
- [Lyn80] J. F. Lynch. Almost sure theories. Annals of Mathematical Logic, 18:91–135, 1980.
- [Pap85] C. H. Papadimitriou. A note on the expressive power of Prolog. Bullentin of the EATCS, 26:21–23, 1985.
- Artificial Intelligence, 81:17–29, 1996.
- [SS88] S. Shelah and J. Spencer. Zero-one laws for sparse random graphs. Journal of the
- American Mathematical Society, 1(1):97–115, 1988.
- [Ull89] J. D. Ullman. Database and knowledge-base systems. Computer Science Press, 1989.

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn