Boolean Satifiability and Beyond: Algorithms, Analysis, and AI Applications
Authors: Matti Järvisalo
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | To illustrate the practical potential of the general framework, going beyond NP, we have shown [Saikko et al., 2016b] that a practical instantiation for the problem of propositional abduction hard for the second-level of the polynomial hierarchy surpasses the efficiency of an approach based on disjunctive answer set programming. A successful approach to AF reasoning is provided by our CEGARTIX system [Dvoˇrák et al., 2014]. Implementing a SAT-based counterexample-guided abstraction refinement approach to second-level complete skeptical and credulous reasoning over AFs, the system ranked at the top in the First International Competition on Computational Models of Argumentation (ICCMA 2015; see http: //argumentationcompetition.org) in beyond-NP problem categories. |
| Researcher Affiliation | Academia | Matti Järvisalo Helsinki Institute for Information Technology HIIT, Department of Computer Science, University of Helsinki, Finland |
| Pseudocode | Yes | Figure 1: Generic implicit hitting set algorithm, which outlines the steps of the approach: Predicate check, K := K [ {C}, Compute S over K, Output S, c(S). |
| Open Source Code | Yes | Going beyond NP, we propose novel counterexample-guided abstraction refinement procedures for the second-level complete problems, as well as an open-source system implementation of the approach. |
| Open Datasets | Yes | In a recent line of research, we have developed new approaches to various data analysis problems, including structure learning of Bayesian networks [Berg et al., 2014; Saikko et al., 2015] and chain graphs [Sonntag et al., 2015], causal discovery and inference [Hyttinen et al., 2013; 2014; 2015], correlation clustering [Berg and Järvisalo, 2016], information visualization [Bunte et al., 2014], and frequent itemset mining [Järvisalo, 2011], based on SAT and Boolean optimization solvers. |
| Dataset Splits | No | The paper discusses various experimental results and applications but does not provide specific details on training, validation, or test dataset splits (e.g., percentages, sample counts, or explicit splitting methodology). |
| Hardware Specification | No | The paper is an overview of research contributions and does not provide specific hardware details (e.g., CPU/GPU models, memory) used for running experiments. |
| Software Dependencies | No | The paper mentions various software components and solvers such as 'SAT solver technology', 'SMT', 'IP solvers', 'Max SAT solvers', 'LMHS', and 'CEGARTIX system', but does not provide specific version numbers for any of them. |
| Experiment Setup | No | The paper provides an overview of research and results but does not contain specific experimental setup details such as hyperparameter values, training configurations, or system-level settings. |