Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Classical Generalized Probabilistic Satisfiability
Authors: Carlos Caleiro, Filipe Casal, Andreia Mordido
IJCAI 2017 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Here, we present a polynomial reduction of GGen PSAT to SMT over the quantifierfree theory of linear integer and real arithmetic. Capitalizing on this translation, we implement and test a solver for the GGen PSAT problem. As previously observed for many other NP-complete problems, we are able to detect a phase transition behavior for GGen PSAT. |
| Researcher Affiliation | Academia | Carlos Caleiro SQIG Instituto de Telecomunicac oes DMath, Instituto Superior T ecnico Universidade de Lisboa, Portugal EMAIL Filipe Casal CMAF-CIO, Portugal DMath, Instituto Superior T ecnico Universidade de Lisboa, Portugal filipeEMAIL Andreia Mordido INOV INESC Inovac ao, Portugal EMAIL |
| Pseudocode | Yes | Algorithm 1 GGen PSAT solver based on SMT QF LIRA |
| Open Source Code | Yes | [Caleiro et al., 2016c] C. Caleiro, F. Casal, and A. Mordido. GGen PSAT solver, 2016. Available online at https://github.com/fcasal/ggenpsat.git. |
| Open Datasets | No | The paper mentions generating 'random GGen PSAT instances' and 'random 3SAT instances' but does not specify access information (link, citation, DOI) for these generated datasets. |
| Dataset Splits | No | The paper mentions generating 'random GGen PSAT instances' but does not specify any training, validation, or test splits for these instances. |
| Hardware Specification | Yes | The machine used for the tests was a Mac Pro at 3.33 GHz 6-Core Intel Xeon with 6 GB of memory. |
| Software Dependencies | Yes | The software was written in Python, and we used Yices [Dutertre, 2014], version 2.5.1, to solve the SMT problem. |
| Experiment Setup | Yes | We generated the random GGen PSAT instances as follows: a random 3SAT instance with n variables and m clauses is generated and then, each variable xi is replaced by a problem Gi which is a conjunction of k random probabilistic atoms over n variables. |