{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T02:06:27Z","timestamp":1768701987249,"version":"3.49.0"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2015,6,25]],"date-time":"2015-06-25T00:00:00Z","timestamp":1435190400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1007\/s10472-015-9466-6","type":"journal-article","created":{"date-parts":[[2015,6,24]],"date-time":"2015-06-24T11:10:18Z","timestamp":1435144218000},"page":"351-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Probabilistic satisfiability: algorithms with the presence and absence of a phase transition"],"prefix":"10.1007","volume":"75","author":[{"given":"Marcelo","family":"Finger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Glauber","family":"De Bona","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,25]]},"reference":[{"issue":"1","key":"9466_CR1","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1023\/A:1012332915908","volume":"33","author":"K Andersen","year":"2001","unstructured":"Andersen, K., Pretolani, D.: Easy cases of probabilistic satisfiability. Ann. Math. Artif. Intell. 33(1), 69\u201391 (2001)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9466_CR2","unstructured":"Andrade, P.S.S., Rocha, J., Couto, D.P., da Costa Teves, A., Cozman, F.: A toolset for propositional probabilistic logic. In: Dutra, I. de C. (ed.) ENIA 2007 (2007)"},{"issue":"2","key":"9466_CR3","first-page":"81","volume":"4","author":"M Baioletti","year":"2000","unstructured":"Baioletti, M., Capotorti, A., Tulipani, S., Vantaggi, B.: Elimination of boolean variables for probabilistic coherence. Soft Computing-A Fusion of Foundations. Methodologies Appl. 4(2), 81\u201388 (2000)","journal-title":"Methodologies Appl."},{"issue":"1","key":"9466_CR4","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1023\/A:1014585822798","volume":"35","author":"M Baioletti","year":"2002","unstructured":"Baioletti, M., Capotorti, A., Tulipani, S., Vantaggi, B.: Simplification rules for the coherent probability assessment problem. Ann. Math. Artif. Intell. 35(1), 11\u201328 (2002)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9466_CR5","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825\u2013885 (2009)"},{"key":"9466_CR6","unstructured":"Bertsimas, D., Tsitsiklis, J.N.: Introduction to linear optimization. Athena Scientific (1997)"},{"key":"9466_CR7","volume-title":"An Investigation on the Laws of Thought. Macmillan","author":"G Boole","year":"1854","unstructured":"Boole, G.: An Investigation on the Laws of Thought. Macmillan. Available on project Gutemberg at, London (1854). http:\/\/www.gutenberg.org\/etext\/15114"},{"key":"9466_CR8","doi-asserted-by":"crossref","unstructured":"Borgward, K.H.: The Simplex Method: A Probabilistic Analysis. Algorithms and Combinatorics 1. Springer (1986)","DOI":"10.1007\/978-3-642-61578-8"},{"key":"9466_CR9","unstructured":"Cheeseman, P., Kanefsky, B., Taylor, W.M.: Where the really hard problems are. In: 12th IJCAI, pp. 331\u2013337. Morgan Kaufmann 1991. http:\/\/portal.acm.org\/citation.cfm?id=1631171.1631221"},{"key":"9466_CR10","doi-asserted-by":"crossref","unstructured":"Coletti, G., Scozzafava, R.: Probabilistic Logic in a Coherent Setting. Trends in Logic, Vol. 15: Studia Logica Library. Kluwer Academic Publishers (2002)","DOI":"10.1007\/978-94-010-0474-9"},{"key":"9466_CR11","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Conference Record of Third Annual ACM Symposium on Theory of Computing STOC, pp. 151\u2013158. ACM (1971)","DOI":"10.1145\/800157.805047"},{"key":"9466_CR12","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/j.ijar.2014.09.002","volume":"58","author":"FG Cozman","year":"2014","unstructured":"Cozman, F.G., di Ianni, L.F.: Probabilistic satisfiability and coherence checking through integer programming. Int. J. Approx. Reason. 58, 57\u201370 (2014)","journal-title":"Int. J. Approx. Reason."},{"key":"9466_CR13","volume-title":"Theory of Probability, vol. 1","author":"deB Finetti","year":"1974","unstructured":"Finetti, de B.: Theory of Probability, vol. 1. Wiley, London (1974)"},{"key":"9466_CR14","doi-asserted-by":"crossref","unstructured":"Eckhoff, J., Helly, Radon: Caratheodory type theorems. In: Gruber, P.M., Wills, J.M. (eds.) Handbook of Convex Geometry, pp. 389\u2013448. Elsevier Science Publishers (1993)","DOI":"10.1016\/B978-0-444-89596-7.50017-1"},{"key":"9466_CR15","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"1-4","key":"9466_CR16","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1-4), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"9466_CR17","doi-asserted-by":"crossref","unstructured":"Finger, M., De Bona, G.: A refuted conjecture on probabilistic satisfiability. In: SBIA, pp. 293\u2013302 (2010)","DOI":"10.1007\/978-3-642-16138-4_30"},{"key":"9466_CR18","unstructured":"Finger, M., De Bona, G.: Probabilistic satisfiability: Logic-based algorithms and phase transition (2011)"},{"key":"9466_CR19","doi-asserted-by":"crossref","unstructured":"Finger, M., Le Bras, R., Gomes, C.P., Selman, B.: Solutions for hard and soft constraints using optimized probabilistic satisfiability. In: Theory and Applications of Satisfiability Testing\u2013SAT 2013, pp. 233\u2013249. Springer (2013)","DOI":"10.1007\/978-3-642-39071-5_18"},{"key":"9466_CR20","doi-asserted-by":"crossref","unstructured":"Garling, D.J.H.: Inequalities: A Journey into Linear Analysis. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511755217"},{"key":"9466_CR21","unstructured":"Gent, I.P., Walsh, T.: The SAT phase transition. In: ECAI94 \u2013 Proceedings of the Eleventh European Conference on Artificial Intelligence, pp. 105\u2013109. John Wiley & Sons (1994)"},{"key":"9466_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0885-064X(88)90006-4","volume":"41","author":"G Georgakopoulos","year":"1988","unstructured":"Georgakopoulos, G., Kavvadias, D., Papadimitriou, C.H.: Probabilistic satisfiability. J. Complex. 41, 1\u201311 (1988)","journal-title":"J. Complex."},{"issue":"3","key":"9466_CR23","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1305\/ndjfl\/1093870625","volume":"25","author":"T Hailperin","year":"1984","unstructured":"Hailperin, T.: Probability logic Notre Dame . J. Form. Log. 25(3), 198\u2013212 (1984)","journal-title":"J. Form. Log."},{"key":"9466_CR24","volume-title":"Boole\u2019s Logic and Probability, Studies in Logic and the Foundations of Mathematics, vol. 85, second enlarged edn","author":"T Hailperin","year":"1986","unstructured":"Hailperin, T.: Boole\u2019s Logic and Probability, Studies in Logic and the Foundations of Mathematics, vol. 85, second enlarged edn. North-Holland, Amsterdam (1986)"},{"key":"9466_CR25","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BF02241270","volume":"44","author":"P Hansen","year":"1990","unstructured":"Hansen, P., Jaumard, B.: Algorithms for the maximum satisfiability problem. Comput. 44, 279\u2013303 (1990)","journal-title":"Comput."},{"key":"9466_CR26","doi-asserted-by":"crossref","unstructured":"Hansen, P., Jaumard, B.: Probabilistic satisfiability. In: Handbook of Defeasible Reasoning and Uncertainty Management Systems. Vol.5, p. 321. Springer Netherlands (2000)","DOI":"10.1007\/978-94-017-1737-3_8"},{"key":"9466_CR27","unstructured":"Hansen, P., Jaumard, B., Arag\u00e3o, de M.P., Chauny, F., Perron, S.: Probabilistic satisfiability with imprecise probabilities. In: 1st International Symposium on Imprecise Probabilities and Their Applications, pp165\u2013174 (1999)"},{"key":"9466_CR28","unstructured":"Hansen, P., Jaumard, B., Nguets\u00e9, G.B.D., Arag\u00e3o, de M.P.: Models and algorithms for probabilistic and bayesian logic. In: IJCAI, pp 1862\u20131868 (1995)"},{"issue":"2","key":"9466_CR29","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.ijar.2007.03.001","volume":"47","author":"P Hansen","year":"2008","unstructured":"Hansen, P., Perron, S.: Merging the local and global approaches to probabilistic satisfiability. Int. J. Approx. Reason. 47(2), 125\u2013140 (2008)","journal-title":"Int. J. Approx. Reason."},{"key":"9466_CR30","unstructured":"Heule, M., van Maaren, H.: march hi: solver description. In: SAT Competition, pp. 27\u201328 (2009)"},{"issue":"2","key":"9466_CR31","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1287\/ijoc.3.2.135","volume":"3","author":"B Jaumard","year":"1991","unstructured":"Jaumard, B., Hansen, P., Arag\u00e3o, de M.P.: Column generation methods for probabilistic logic. INFORMS J. Comput. 3(2), 135\u2013148 (1991)","journal-title":"INFORMS J. Comput."},{"key":"9466_CR32","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF01531078","volume":"1","author":"D Kavvadias","year":"1990","unstructured":"Kavvadias, D., Papadimitriou, C.H.: A linear programming approach to reasoning about probabilities. Ann. Math. Artif. Intell. 1, 189\u2013205 (1990)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9466_CR33","doi-asserted-by":"crossref","unstructured":"Klinov, P., Parsia, B.: A hybrid method for probabilistic satisfiability. In: Automated Deduction\u2013CADE-23, pp. 354\u2013368. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_27"},{"key":"9466_CR34","doi-asserted-by":"crossref","unstructured":"Klinov, P., Parsia, B.: Pronto: A practical probabilistic description logic reasoner. In: Uncertainty Reasoning for the Semantic Web II (URSW), LNCS, vol. 7123, pp. 59\u201379. Springer (2013)","DOI":"10.1007\/978-3-642-35975-0_4"},{"key":"9466_CR35","doi-asserted-by":"crossref","unstructured":"Klinov, P., Parsia, B., Mui\u00f1o, D.P.: The consistency of the medical expert system cadiag-2: A probabilistic approach. Interdiscip. Adv.Inf. Technol. Res., 1 (2013)","DOI":"10.4018\/978-1-4666-3625-5.ch001"},{"issue":"3","key":"9466_CR36","first-page":"265","volume":"9","author":"LA Levin","year":"1973","unstructured":"Levin, L.A.: Universal search problems. Probl. Inf. Transm. 9(3), 265\u2013266 (1973)","journal-title":"Probl. Inf. Transm."},{"key":"9466_CR37","doi-asserted-by":"crossref","unstructured":"Li, C., Manya, F., Mohamedou, N., Planes, J.: Exploiting cycle structures in Max-SAT. In: Theory and Applications of Satisfiability Testing \u2014 SAT, pp. 467\u2013480. Springer (2009)","DOI":"10.1007\/978-3-642-02777-2_43"},{"key":"9466_CR38","unstructured":"Marques-Silva, J.: The MSUNCORE MAXSAT solver. In: SAT competition, pp. 151\u2013152 (2009)"},{"key":"9466_CR39","doi-asserted-by":"crossref","unstructured":"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, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"9466_CR40","doi-asserted-by":"crossref","unstructured":"de Moura, L.M.: Z3: An efficient SMT solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"9466_CR41","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0004-3702(86)90031-7","volume":"28","author":"N Nilsson","year":"1986","unstructured":"Nilsson, N.: Probabilistic logic. Artif. Intell. 28(1), 71\u201387 (1986)","journal-title":"Artif. Intell."},{"issue":"1\u20132","key":"9466_CR42","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/0004-3702(93)90167-A","volume":"59","author":"N Nilsson","year":"1993","unstructured":"Nilsson, N.: Probabilistic logic revisited. Artif. Intell. 59(1\u20132), 39\u201342 (1993)","journal-title":"Artif. Intell."},{"key":"9466_CR43","unstructured":"Odifreddi, P.: Classical Recursion Theory, Studies in Logic and the Foundations of Mathematics, vol. 125. Elsevier (1989)"},{"key":"9466_CR44","unstructured":"Papadimitriou, C., Steiglitz, K.: Combinatorial Optimization: Algorithms and Complexity Dover (1998)"},{"key":"9466_CR45","unstructured":"Prestwich, S.D.: CNF encodings. In: Handbook of Satisfiability, pp. 75\u201397 (2009)"},{"issue":"1-4","key":"9466_CR46","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/s10472-005-0430-8","volume":"43","author":"D Pretolani","year":"2005","unstructured":"Pretolani, D.: Probability Logic and Optimization SAT: The PSAT and CPA Models. Ann. Math. Artif. Intell. 43 (1-4), 211\u2013221 (2005). doi: 10.1007\/s10472-004-9430-3","journal-title":"Ann. Math. Artif. Intell."},{"key":"9466_CR47","unstructured":"Savage, J.E.: The Complexity of Computing. Krieger Publishing Co., Inc., Melbourne, FL USA (1976)"},{"issue":"3-4","key":"9466_CR48","first-page":"141","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. JSAT 3(3-4), 141\u2013224 (2007)","journal-title":"JSAT"},{"key":"9466_CR49","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/s101070100261","volume":"91","author":"MJ Todd","year":"2002","unstructured":"Todd, M.J.: The many facets of linear programming. Math. Program. 91, 417\u2013436 (2002). doi: 10.1007\/s101070100261","journal-title":"Math. Program."},{"issue":"1","key":"9466_CR50","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.jspi.2003.09.005","volume":"126","author":"P Walley","year":"2004","unstructured":"Walley, P., Pelessoni, R., Vicig, P.: Direct algorithms for checking consistency and making inferences from conditional probability assessments. J. Stat. Plan. Infer. 126 (1), 119\u2013151 (2004). doi: 10.1016\/j.jspi.2003.09.005 http:\/\/www.sciencedirect.com\/science\/article\/B6V0M-49TJMSP-1\/2\/ fd1ab649db4753c886c2ad0535b889ea","journal-title":"J. Stat. Plan. Infer."},{"issue":"2","key":"9466_CR51","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"JP Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Inf. Process. Lett. 68(2), 63\u201369 (1998)","journal-title":"Inf. Process. Lett."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-015-9466-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-015-9466-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-015-9466-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,4]],"date-time":"2020-09-04T02:16:39Z","timestamp":1599185799000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-015-9466-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,25]]},"references-count":51,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2015,12]]}},"alternative-id":["9466"],"URL":"https:\/\/doi.org\/10.1007\/s10472-015-9466-6","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,25]]}}}