Personnel Scheduling as Satisfiability Modulo Theories
Authors: Christoph Erkinger, Nysret Musliu
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | These two modeling approaches were experimentally evaluated on benchmark instances from literature using different state-of-the-art SMT-solvers. |
| Researcher Affiliation | Academia | Christoph Erkinger and Nysret Musliu Institute of Information Systems, TU Wien, Austria christoph.erkinger@gmail.com, musliu@dbai.tuwien.ac.at |
| Pseudocode | Yes | Algorithm 1: Wegner’s Method for Hamming Weight |
| Open Source Code | No | The paper refers to '20 benchmark instances described in [Musliu, 2005; 2006].1' with a footnote pointing to 'http://www.dbai.tuwien.ac.at/staff/musliu/benchmarks/workforceScheduling.zip', which is for the benchmark data, not the authors' source code for the SMT modeling approaches. |
| Open Datasets | Yes | In this section we investigate the performance of our two modeling approaches on 20 benchmark instances described in [Musliu, 2005; 2006].1 The first three problems have been used in most rotating workforce scheduling papers given in the introduction and other 17 instances were derived from real life problems of different business areas. The collection contains small, middle-size and very large instances. (...) 1http://www.dbai.tuwien.ac.at/staff/musliu/benchmarks/workforceScheduling.zip |
| Dataset Splits | No | The paper evaluates its approach on '20 benchmark instances' from literature. These are discrete constraint satisfaction problems, not datasets that are typically split into training, validation, and test sets for model training. The goal is to find solutions for these instances, not to train a model on a training set and validate it. |
| Hardware Specification | Yes | The solving process was performed on an Apple Mac Book Pro with the following hardware details: 2.0 GHz quad-core Intel Core i7 (Sandy-Bridge) and 8 GB DDR3 RAM. |
| Software Dependencies | Yes | We applied five state-of-the-art SMT-solvers (Z3 version 4.3.1 [de Moura and Bjørner, 2008], Math SAT5 version 5.2.5 (gmp 5.0.5, clang/LLVM 3.1, 64-bit) [Cimatti et al., 2013], CVC4 version 1.0 (compiled with GCC version 4.2.1) [Barrett et al., 2011], Yices version 2.1.0 [Dutertre and de Moura, 2006] and Boolector version 1.5.115 [Brummayer and Biere, 2009]). |
| Experiment Setup | Yes | The timeout for each solver and instance was set to 1000 seconds. |