On Computational Aspects of Iterated Belief Change
Authors: Nicolas Schwind, Sebastien Konieczny, Jean-Marie Lagniez, Pierre Marquis
IJCAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We also show that a revised belief state can be computed in a reasonable time for large-sized instances using SAT-based algorithms, and we report empirical results showing the feasibility of iterated belief change for bases of significant sizes. |
| Researcher Affiliation | Collaboration | Nicolas Schwind1 , S ebastien Konieczny2 , Jean-Marie Lagniez3 and Pierre Marquis2,4 1National Institute of Advanced Industrial Science and Technology, Tokyo, Japan 2CRIL CNRS, Universit e d Artois, Lens, France 3Huawei Technologies Ltd, Boulogne-Billancourt, France 4Institut Universitaire de France |
| Pseudocode | Yes | Proposition 5. Let Φ = (ϕ1, . . . , ϕn) and α, µ be two formulae. Then |= O can be decided by the following procedure: 1. if ϕ1 µ α |= then return False; 2. if ϕ1 µ |= then return True; 3. if (ϕ1 (ϕ2 µ)) α |= then return False; 4. Return True; |
| Open Source Code | No | Lastly, we will implement some other change operators (especially, those described in [Rott, 2009]) and make the code we developed for generating and querying CWRs available online. |
| Open Datasets | No | The paper describes generating synthetic instances ('3-CNF formulae') for experiments rather than using a pre-existing public dataset with standard training splits. No information about train sets is provided. |
| Dataset Splits | No | The paper describes generating synthetic instances for experiments and does not mention any validation dataset splits. |
| Hardware Specification | Yes | All the experiments have been conducted on a cluster of Intel Xeon E5-2643 (3.30 GHz) quad core processors with 32 Gi B RAM. |
| Software Dependencies | No | The SAT solver used in the experiments is Mini SAT [E en and S orensson, 2003]. However, no specific version number for Mini SAT or other ancillary software is provided. |
| Experiment Setup | Yes | The propositional formulae ϕ and µ considered in our experiments are 3-CNF formulae (i.e., conjunctions of clauses of size at most 3), built using the modularity-based random generator presented in [Gir aldez-Cru and Levy, 2015]. ... for each instance, the 3-CNF formula ϕ considered at start is built over 4048 variables, has 12144 clauses, and is obtained using a modularity of 512, while every change formula µ of the sequence is a 3-CNF formula generated from 814 variables (among the 4048 ones used in ϕ), with 2442 clauses and for a modularity picked up at random between 3 and 50. A time-out of 900s and a memory-out of 7.6 Gi B has been considered for each instance. |