AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
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

Unsatisfiable random formulas are hard to certify

LICS, pp.325-334, (2002)

Cited by: 8|Views128
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.
    Google ScholarLocate open access versionFindings
  • [Ach01] D. Achlioptas. A survey of lower bounds for random 3-SAT via differential equations. Theoretical Computer Science, 265(1–2):159–185, 2001.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [BH79] A. Blass and F. Harary. Properties of almost all graphs and complexes. Journal of Graph Theory, 3:225–240, 1979.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarFindings
  • [BSG01] E. Ben-Sasson and N. Galesi. Space complexity of random formulas in resolution. In 16th IEEE Conference in Computational Complexity, 2001.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [BSW01] E. Ben-Sasson and A. Wigderson. Short proofs are narrow–resolution made simple. Journal of the ACM, 48(2):149–169, 2001.
    Google ScholarLocate open access versionFindings
  • [CR79] S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44:36–50, 1979.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [CS88] V. Chvatal and E. Szemeredi. Many hard examples for resolution. Journal of the ACM, 35(4):759–768, 1988.
    Google ScholarLocate open access versionFindings
  • [Fag76] R. Fagin. Probabilities on finite models. Journal of Symbolic Logic, 41:50–58, 1976.
    Google ScholarLocate open access versionFindings
  • [Hak85] A. Haken. The intractability of resolution. Theoretical Computer Science, 39:297–308, 1985.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [Lyn80] J. F. Lynch. Almost sure theories. Annals of Mathematical Logic, 18:91–135, 1980.
    Google ScholarLocate open access versionFindings
  • [Pap85] C. H. Papadimitriou. A note on the expressive power of Prolog. Bullentin of the EATCS, 26:21–23, 1985.
    Google ScholarLocate open access versionFindings
  • Artificial Intelligence, 81:17–29, 1996.
    Google ScholarLocate open access versionFindings
  • [SS88] S. Shelah and J. Spencer. Zero-one laws for sparse random graphs. Journal of the
    Google ScholarLocate open access versionFindings
  • American Mathematical Society, 1(1):97–115, 1988.
    Google ScholarLocate open access versionFindings
  • [Ull89] J. D. Ullman. Database and knowledge-base systems. Computer Science Press, 1989.
    Google ScholarFindings
Your rating :
0

 

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