Constraint Answer Set Programming versus Satisfiability Modulo Theories
Authors: Yuliya Lierler, Benjamin Susman
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this work we attempt to unify the terminology used in CASP and SMT so that the differences and similarities of logic programs with constraints versus logic programs modulo theories become apparent. At the same time, we introduce the notion of constraint formulas, which are similar to that of logic programs with constraints. We identify a special class of SMT theories that we call uniform . Commonly used theories in satisfiability modulo solving such as integer linear, difference logic, and linear arithmetics belong to uniform theories. This class of theories helps us to establish precise links (i) between constraint formulas and SMT formulas, and (ii) between CASP and SMT. We are able to then provide a formal description relating a family of distinct constraint answer set programming formalisms. |
| Researcher Affiliation | Academia | University of Nebraska at Omaha ylierler@unomaha.edu and bsusman@unomaha.edu |
| Pseudocode | No | The paper presents formal definitions and theorems but does not include any pseudocode or algorithm blocks. |
| Open Source Code | No | The paper discusses various existing CASP and SMT solvers and their underlying technologies but does not provide source code for the theoretical work described in this paper. There is no statement of releasing code or a link to a repository. |
| Open Datasets | No | This is a theoretical paper that does not use datasets or conduct empirical studies. Therefore, it does not provide information about publicly available training data. |
| Dataset Splits | No | This paper is theoretical and does not involve empirical experiments with datasets, thus no dataset split information for training, validation, or testing is provided. |
| Hardware Specification | No | This is a theoretical paper and does not describe any experimental setup or hardware used for computations. |
| Software Dependencies | No | The paper discusses various existing solvers (e.g., CLINGCON, EZCSP, MINGO, DINGO) and their components (e.g., GECODE, BPROLOG, SICSTUS PROLOG, SWI PROLOG, CPLEX, Z3) as part of the related work and landscape analysis, but it does not specify software dependencies with version numbers for reproducing its own theoretical contributions or any experiments conducted by the authors. |
| Experiment Setup | No | This paper is theoretical and focuses on formal links and definitions, not on empirical experiments. Therefore, no experimental setup details such as hyperparameters or system-level training settings are provided. |