An Upper Bound on the Space Complexity of Random Formulae in Resolution

Michele Zito

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 36, Issue: 4, page 329-339
  • ISSN: 0988-3754

Abstract

top
We prove that, with high probability, the space complexity of refuting a random unsatisfiable Boolean formula in k-CNF on n variables and m = Δn clauses is O n · Δ - 1 k - 2 .

How to cite

top

Zito, Michele. "An Upper Bound on the Space Complexity of Random Formulae in Resolution." RAIRO - Theoretical Informatics and Applications 36.4 (2010): 329-339. <http://eudml.org/doc/92705>.

@article{Zito2010,
abstract = { We prove that, with high probability, the space complexity of refuting a random unsatisfiable Boolean formula in k-CNF on n variables and m = Δn clauses is $O\left(n \cdot \Delta^\{-\frac\{1\}\{k-2\}\}\right)$. },
author = {Zito, Michele},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Random formulae; space complexity; satisfiability threshold.; satisfiability threshold; random unsatisfiable Boolean formula},
language = {eng},
month = {3},
number = {4},
pages = {329-339},
publisher = {EDP Sciences},
title = {An Upper Bound on the Space Complexity of Random Formulae in Resolution},
url = {http://eudml.org/doc/92705},
volume = {36},
year = {2010},
}

TY - JOUR
AU - Zito, Michele
TI - An Upper Bound on the Space Complexity of Random Formulae in Resolution
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 36
IS - 4
SP - 329
EP - 339
AB - We prove that, with high probability, the space complexity of refuting a random unsatisfiable Boolean formula in k-CNF on n variables and m = Δn clauses is $O\left(n \cdot \Delta^{-\frac{1}{k-2}}\right)$.
LA - eng
KW - Random formulae; space complexity; satisfiability threshold.; satisfiability threshold; random unsatisfiable Boolean formula
UR - http://eudml.org/doc/92705
ER -

References

top
  1. D. Achlioptas and G.B. Sorkin, Optimal myopic algorithms for random 3-SAT, in 41st Annual Symposium on Foundations of Computer Science (2000) 590-600.  
  2. M. Alekhnovich, E. Ben-Sasson, A.A. Razborov and A. Wigderson, Space complexity in propositional calculus, in Proc. of the 32nd Annual ACM Symposium on Theory of Computing. Portland, OR (2000).  
  3. P. Beame, R. Karp, T. Pitassi and M. Saks, On the complexity of unsatisfiability proofs for random k-CNF formulas, in Proc. of the 30th Annual ACM Symposium on Theory of Computing. New York (1998) 561-571.  
  4. E. Ben-Sasson and N. Galesi, Space complexity of random formulae in resolution, in Proc. of the 16th Annual IEEE Conference on Computational Complexity. IEEE Computer Society (2001).  
  5. B. Bollobás, C. Borgs, J.T. Chayes, J.H. Kim and D.B. Wilson, The scaling window of the 2-SAT transition. Random Structures Algorithms18 (2001) 201-256.  
  6. P. Cheeseman, B. Kanefsky and W.M. Taylor, Where the really hard problems are, in Proc. of IJCAI-91, edited by Kauffmann (1991) 331-337.  
  7. V. Chvátal and E. Szemerédi, Many hard examples for resolution. J. ACM35 (1988) 759-768.  
  8. S.A. Cook and R. Reckhow, The relative efficiency of propositional proof systems. J. Symb. Logic44 (1979) 36-50.  
  9. M. Davis, G. Logemann and D. Loveland, A machine program for theorem proving. Commun. ACM5 (1962) 394-397.  
  10. M. Davis and H. Putnam, A computing procedure for quantification theory. J. ACM7 (1960) 201-215.  
  11. J. Esteban and J.L. Toran, Space bounds for resolution, edited by C. Meinel and S. Tison, in STACS 99: 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 1999, Proceedings. Springer-Verlag, Lecture Notes in Comput. Sci. 1563 (1999) 551-560.  
  12. A. Goerdt, A threshold for unsatisfiability. J. Comput. System Sci.53 (1996) 469-486.  
  13. T. Hagerup and C. Rüb, A guided tour of Chernoff bounds. Inform. Process. Lett.33 (1989) 305-308.  
  14. A.C. Kaporis, L.M. Kirousis, Y.C. Stamatiou, M. Vamvakari and M. Zito, Coupon collectors, q-binomial coefficients and the unsatisfiability threshold, edited by A. Restivo, S. Ronchi della Rocca and L. Roversi. Theoret. Comput. Sci., in 7th Italian Conference, ICTCS 2001. Springer-Verlag, Lecture Notes in Comput. Sci. 2202 (2001) 328-338.  
  15. R. Bruce King, Beyond the quartic equation. Birkhauser, Boston, MA (1996).  
  16. R. Bruce King and E. Rodney Canfield, An algorithm for calculating the roots of a general quintic equation from its coefficients. J. Math. Phys.32 (1991) 823-825.  
  17. I. Stewart, Galois Theory. Chapman and Hall, London (1973).  
  18. J. Toran, Lower bounds for the space used in resolution, edited by J. Flum and M. Rodriguez-Artalejo, in Computer Science Logic: 13th International Workshop, CSL'99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings. Springer-Verlag, Lecture Notes in Comput. Sci. 1683 (1999).  
  19. B.L. van der Wärden, Algebra. Frederick Ungar Publishing Co., New York (1970).  
  20. R.C. Weast, Handbook of Tables for Mathematics. Cleveland: The Chemical Rubber Co. (1964).  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.