Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Finger, Marcelo; Reis, Poliana (2013)
Publisher: Multidisciplinary Digital Publishing Institute
Journal: Information
Languages: English
Types: Article
Subjects: Information technology, landscape of distributions, SAT, T58.5-58.64, SAT solver, phase transition

Classified by OpenAIRE into

arxiv: Computer Science::Logic in Computer Science
In this work we provide a statistical form of empirical analysis of classical propositional logic decision methods called SAT solvers. This work is perceived as an empirical counterpart of a theoretical movement, called the enduring scandal of deduction, that opposes considering Boolean Logic as trivial in any sense. For that, we study the predictability of classical logic, which we take to be the distribution of the runtime of its decision process. We present a series of experiments that determines the run distribution of SAT solvers and discover a varying landscape of distributions, following the known existence of a transition of easy-hard-easy cases of propositional formulas. We find clear distributions for the easy areas and the transitions easy-hard and hard-easy. The hard cases are shown to be hard also for the detection of statistical distributions, indicating that several independent processes may be at play in those cases.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 1. D'Agostino, M.; Floridi, L. The enduring scandal of deduction. Is propositional logic really uninformative? Synthese 2009, 167, 271-315.
    • 2. Hintikka, J. Logic, Language Games and Information. Kantian Themes in the Philosophy of Logic; Clarendon Press: Oxford, UK, 1973.
    • 3. Dummett, M. The Logical Basis of Metaphysics; Duckworth: London, UK, 1991.
    • 4. Floridi, L. Is information meaningful data? Philos. Phenomen. Res. 2005, 70, 351-370.
    • 5. Cook, S.A. The Complexity of Theorem-Proving Procedures. In Conference Record of Third Annual ACM Symposium on Theory of Computing (STOC); ACM: Cincinnati, OH, USA, 1971; pp. 151-158.
    • 6. Papadimitriou, C.H. Computational Complexity; Addison-Wesley: Boston, MA, USA, 1994.
    • 7. Arora, S.; Barak, B. Computational Complexity: A Modern Approach, 1st ed.; Cambridge University Press: Cambridge, UK, 2009.
    • 8. Schaerf, M.; Cadoli, M. Tractable Reasoning via Approximation. Artif. Intell. 1995, 74, 249-310.
    • 9. Dalal, M. Anytime Families of Tractable Propositional Reasoners. In International Symposium of Artificial Intelligence and Mathematics AI/MATH-96, Fort Lauderdale, FL, USA, 1996; pp. 42-45.
    • 10. Finger, M.; Wassermann, R. Approximate and Limited Reasoning: Semantics, Proof Theory, Expressivity and Control. J. Logic Comput. 2004, 14, 179-204.
    • 11. Finger, M.; Gabbay, D. Cut and Pay. J. Log. Lang. Inf. 2006, 15, 195-218.
    • 12. Finger, M.; Wassermann, R. The Universe of Propositional Approximations. Theor. Comp. Sci. 2006, 355, 153-166.
    • 13. The international SAT Competitions web page. Available online: http://www.satcompetition.org/ (accessed on 31 December 2012).
    • 14. These very large problems arise from industrial applications or may be randomly generated.
    • 15. Gent, I.P.; Walsh, T. The SAT Phase Transition. ECAI94-Proceedings of the Eleventh European Conference on Artificial Intelligence; John Wiley & Sons: Amsterdam, The Netherlands, 1994; pp. 105-109.
    • 16. Mitchell, D.; Selman, B.; Levesque, H. Hard and Easy Distributions of SAT Problems. AAAI92- Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, CA, USA, 1992; pp. 459-465.
    • 17. Moskewicz, M.W.; Madigan, C.F.; Zhao, Y.; Zhang, L.; Malik, S. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC'01), Las Vegas, NV, USA, 2001; pp. 530-535.
    • 18. Goldberg, E.; Novikov, Y. Berkmin: A Fast and Robust SAT Solver. Design Automation and Test in Europe (DATE2002), Paris, France, 2002; pp. 142-149.
    • 19. Ee´n, N.; S o¨rensson, N. An Extensible SAT-solver. SAT 2003, LNCS; Springer: Portofino, Italy, 2003; Volume 2919, pp. 502-518.
    • 20. Available on: http://www.princeton.edu/ chaff/zchaff/zchaff.64bit.2007.3.12.zip (accessed on 7 January 2013).
    • 21. Cheeseman, P.; Kanefsky, B.; Taylor, W.M. Where the really hard problems are. 12th IJCAI; Morgan Kaufmann: Sydney, Australia, 1991; pp. 331-337.
    • 22. Taylor, J. An Introduction to Error Analysis: The Study of Uncertainties in Physical Measurements; Physics-chemistry-engineering, University Science Books: Sausalito, CA, USA, 1997.
    • 23. Minitab. Available online: http://minitab.com (accessed on 31 December 2012).
    • 24. Reis, P.M. Analysis of Runtime Distributions in SAT solvers (in Portuguese). Master's Thesis, Department of Computer Science, Institute of Mathematics and Statistics, University of Sa˜o Paulo, Sao Paulo, Brazil, 2012.
    • 25. Limpert, E.; Stahel, W.A.; Abbt, M. Log-normal distributions across the sciences: Keys and clues. BioScience 2001, 51, 341-352.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article