On the Predictability of Classical Propositional Logic

Other literature type, Article English OPEN
Finger, Marcelo ; Reis, Poliana (2013)
  • Publisher: Multidisciplinary Digital Publishing Institute
  • Journal: Information (issn: 2078-2489)
  • Related identifiers: doi: 10.3390/info4010060
  • Subject: Information technology | landscape of distributions | SAT | T58.5-58.64 | SAT solver | phase transition
    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.
  • References (25)
    25 references, page 1 of 3

    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.

  • Metrics
    No metrics available
Share - Bookmark