{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T22:11:53Z","timestamp":1760220713990,"version":"build-2065373602"},"reference-count":25,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2013,1,14]],"date-time":"2013-01-14T00:00:00Z","timestamp":1358121600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information"],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.3390\/info4010060","type":"journal-article","created":{"date-parts":[[2013,1,15]],"date-time":"2013-01-15T02:36:29Z","timestamp":1358217389000},"page":"60-74","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the Predictability of Classical Propositional Logic"],"prefix":"10.3390","volume":"4","author":[{"given":"Marcelo","family":"Finger","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Sao Paulo, Sao Paulo, 05508-090, Brazil"}]},{"given":"Poliana","family":"Reis","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Sao Paulo, Sao Paulo, 05508-090, Brazil"}]}],"member":"1968","published-online":{"date-parts":[[2013,1,14]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/s11229-008-9409-4","article-title":"The enduring scandal of deduction. Is propositional logic really uninformative?","volume":"167","author":"Floridi","year":"2009","journal-title":"Synthese"},{"unstructured":"Hintikka, J. (1973). Logic, Language Games and Information. Kantian Themes in the Philosophy of Logic, Clarendon Press.","key":"ref_2"},{"unstructured":"Dummett, M. (1991). The Logical Basis of Metaphysics, Duckworth.","key":"ref_3"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1111\/j.1933-1592.2005.tb00531.x","article-title":"Is information meaningful data?","volume":"70","author":"Floridi","year":"2005","journal-title":"Philos. Phenomen. Res."},{"unstructured":"Cook, S.A. (1971). Conference Record of Third Annual ACM Symposium on Theory of Computing (STOC), ACM.","key":"ref_5"},{"unstructured":"Papadimitriou, C.H. (1994). Computational Complexity, Addison-Wesley.","key":"ref_6"},{"doi-asserted-by":"crossref","unstructured":"Arora, S., and Barak, B. (2009). Computational Complexity: A Modern Approach, Cambridge University Press. [1st].","key":"ref_7","DOI":"10.1017\/CBO9780511804090"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0004-3702(94)00009-P","article-title":"Tractable Reasoning via Approximation","volume":"74","author":"Schaerf","year":"1995","journal-title":"Artif. Intell."},{"unstructured":"Dalal, M. International Symposium of Artificial Intelligence and Mathematics AI\/MATH-96, Fort Lauderdale.","key":"ref_9"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1093\/logcom\/14.2.179","article-title":"Approximate and Limited Reasoning: Semantics, Proof Theory, Expressivity and Control","volume":"14","author":"Finger","year":"2004","journal-title":"J. Logic Comput."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10849-005-9001-y","article-title":"Cut and Pay","volume":"15","author":"Finger","year":"2006","journal-title":"J. Log. Lang. Inf."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/j.tcs.2006.01.007","article-title":"The Universe of Propositional Approximations","volume":"355","author":"Finger","year":"2006","journal-title":"Theor. Comp. Sci."},{"unstructured":"The international SAT Competitions web page. Available online:http:\/\/www.satcompetition.org\/.","key":"ref_13"},{"unstructured":"These very large problems arise from industrial applications or may be randomly generated.","key":"ref_14"},{"unstructured":"Gent, I.P., and Walsh, T. The SAT Phase Transition. ECAI94\u2014Proceedings of the Eleventh European Conference on Artificial Intelligence.","key":"ref_15"},{"unstructured":"Mitchell, D., Selman, B., and Levesque, H. (,  1992). Hard and Easy Distributions of SAT Problems. AAAI92\u2014 Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, CA, USA.","key":"ref_16"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., and Malik, S. (,  2001). Chaff: Engineering an Efficient SAT Solver. Proceedings of the 38th Design Automation Conference (DAC\u201901), as Vegas, NV, USA,.","key":"ref_17","DOI":"10.1145\/378239.379017"},{"unstructured":"Goldberg, E., and Novikov, Y. (2002). Design Automation and Test in Europe (DATE2002).","key":"ref_18"},{"doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., and S\u00f6rensson, N. (2003). An Extensible SAT-solver. SAT 2003, LNCS, Springer.","key":"ref_19","DOI":"10.1007\/978-3-540-24605-3_37"},{"unstructured":"Available online:http:\/\/www.princeton.edu\/\u223cchaff\/zchaff\/zchaff.64bit.2007.3.12.zip.","key":"ref_20"},{"unstructured":"Cheeseman, P., Kanefsky, B., and Taylor, W.M. (1991). 12th IJCAI, Morgan Kaufmann.","key":"ref_21"},{"unstructured":"Taylor, J. (1997). An Introduction to Error Analysis: The Study of Uncertainties in Physical Measurements, Physics-chemistry-engineering, University Science Books.","key":"ref_22"},{"unstructured":"Minitab. Available online:http:\/\/minitab.com.","key":"ref_23"},{"unstructured":"Reis, P.M. (2012). Analysis of Runtime Distributions in SAT solvers (in Portuguese). [Master\u2019s Thesis, Department of Computer Science, Institute of Mathematics and Statistics, University of S\u00e3o Paulo].","key":"ref_24"},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1641\/0006-3568(2001)051[0341:LNDATS]2.0.CO;2","article-title":"Log-normal distributions across the sciences: Keys and clues","volume":"51","author":"Limpert","year":"2001","journal-title":"BioScience"}],"container-title":["Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2078-2489\/4\/1\/60\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T21:44:14Z","timestamp":1760219054000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2078-2489\/4\/1\/60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,14]]},"references-count":25,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2013,3]]}},"alternative-id":["info4010060"],"URL":"https:\/\/doi.org\/10.3390\/info4010060","relation":{},"ISSN":["2078-2489"],"issn-type":[{"type":"electronic","value":"2078-2489"}],"subject":[],"published":{"date-parts":[[2013,1,14]]}}}