Classical Generalized Probabilistic Satisfiability
Authors: Carlos Caleiro, Filipe Casal, Andreia Mordido
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | 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 carlos.caleiro@tecnico.ulisboa.pt Filipe Casal CMAF-CIO, Portugal DMath, Instituto Superior T ecnico Universidade de Lisboa, Portugal filipe.casal@tecnico.ulisboa.pt Andreia Mordido INOV INESC Inovac ao, Portugal andreia.mordido@inov.pt |
| 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. |