SAT Encodings for Distance-Based Belief Merging Operators
Authors: Sbastien Konieczny, Jean-Marie Lagniez, Pierre Marquis
AAAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments have shown the benefits which can be gained by considering the SAT encoding schemes we pointed out. Especially, thanks to them, we succeeded in computing query-equivalent formulae for merging instances based on hundreds of variables, which are out of reach of previous implementations. Another contribution of the paper is the description of a number of benchmarks, obtained by generating instances of a time-tabling problem, then translating them into instances of the merging problem. Finally, a last contribution of this work consists of an empirical evaluation of the encoding schemes we have introduced, showing significant computational benefits. |
| Researcher Affiliation | Academia | S ebastien Konieczny and Jean-Marie Lagniez and Pierre Marquis CRIL, U. Artois & CNRS, F-62300 Lens, France {konieczny, lagniez, marquis}@cril.fr |
| Pseudocode | No | The paper describes the encoding schemes and compilation process in descriptive text but does not include formal pseudocode or algorithm blocks. |
| Open Source Code | Yes | Additional ressources (a detailed example, some empirical results, the time-tabling benchmarks used in our experiments, the generator of time-tabling instances, the translator into instances of belief merging, and the compiler of such instances into CNF encodings) are available on-line from http://www.cril.fr/KC. |
| Open Datasets | Yes | To deal with it, we turned some timetabling benchmarks into distance-based merging ones; we considered instances of the time-tabling problem described in (Bonutti et al. 2012). ... Additional ressources (a detailed example, some empirical results, the time-tabling benchmarks used in our experiments... ) are available on-line from http://www.cril.fr/KC. |
| Dataset Splits | No | The paper focuses on generating and evaluating on 'instances' or 'benchmarks' of a time-tabling problem, rather than splitting a dataset into traditional training, validation, and test sets. |
| Hardware Specification | Yes | Our experiments have been conducted on Intel Xeon E5-2643 (3.30GHz) processors with 32 Gi B RAM on Linux Cent OS. |
| Software Dependencies | No | The paper mentions using 'Max HS' and 'cnf2obdd' but does not provide specific version numbers for these software components, which are required for reproducibility. |
| Experiment Setup | Yes | The non-availability of merging benchmarks corresponding to an actual application was a difficulty we had to face. To deal with it, we turned some timetabling benchmarks into distance-based merging ones... We allocated 900s CPU time and 8 Gi B of memory per instance. ... the number of periods per day (1 ... 4), the number of courses per teacher (1 ... 4), the number of lectures per course (1 ... 4), the number of days when the lectures of a given course are scheduled (1 ... 4), the number of students attending a given course (30 ... 60), the rooms capacities (20 ... 80), the number of courses per curriculum (3 ... 7), the number of curricula (5, 7, 9, 11, 13, 15). For each course, for each period, the probability that the course can be scheduled during the period is set to 50%, and for each room, the probability that the room is suitable to the course is set to 50%. |