Automatic Scheduling of Periodic Event Networks by SAT Solving
In this paper, periodic event scheduling problems (PESP) are encoded as satisfiability problems (SAT) and solved by a state-of-the-art SAT solver. Both the encoding, based on order encoded domains, and the valid use in terms of a proof are presented. The
- PDF / 220,107 Bytes
- 6 Pages / 439.37 x 666.142 pts Page_size
- 59 Downloads / 206 Views
1 Introduction Computing a time table for a given railway network is based on periodic events and constraints imposed on these events. Events and their constraints can be modeled by so-called periodic event networks. The periodic event scheduling problem (PESP) consists of such a network and is the decision problem, whether all the events can be scheduled such that a set of constraints—specified by the network—is satisfied. The problem is NP-complete [9] and the currently best solutions are obtained by constraint-based solvers [7, 8] or by LP solvers, which solve linearized PESP instances by introducing modulo parameters [6]. However, these solvers are still quite limited in the size of the problem that they can tackle, which will be discussed in the results section. In recent years, the performance of SAT solvers has been significantly increased and SAT solvers are now applied in real-world settings such as hardware verification or planning [1]. Hence, the question arises how state-of-the-art SAT solvers perform on encoded periodic event scheduling problems. After introducing SAT and PESP in the preliminaries presented in Sect. 2, the encoding is discussed in Sect. 3, followed by a soundness and completeness proof. In Sect. 4, several real-world instances are presented to a state-of-the-art PESP solver [7] and a state-of-the-art SAT solver. The results indicate, that the SAT approach is by far superior to the PESP solver. The paper is concluded in Sect. 5 by a short discussion and an outline of future work.
P. Großmann (B) TU Dresden, Chair of Traffic Flow Science, Dresden, Germany e-mail: [email protected] S. Helber et al. (eds.), Operations Research Proceedings 2012, Operations Research Proceedings, DOI: 10.1007/978-3-319-00795-3_72, © Springer International Publishing Switzerland 2014
481
482
P. Großmann
2 Notations and Preliminaries Both the satisfiability problem (SAT) and the periodic event scheduling problem (PESP) will be introduced in this section.
2.1 Satisfiability Problem A satisfiability problem (SAT) consists of a propositional formula F and is the decision problem whether it exists an interpretation (or assignment) J from the set of propositional formulas to the set {, ⊥} of truth values such that J assigns to F. In such a case, J is called model for F (J |= F) and F is said to be satisfiable. SAT is NP-complete [2]. It is well-known, that each propositional formula can be transformed into a semantically equivalent formula in conjunctive normal form (CNF), where a formula F = C1 , . . . Cm is in CNF if it is a conjunction of m clauses, a clause C = [L 1 , . . . , L n ] is a disjunction of n literals, and a literal L is either an atom p or the negation of an atom ¬ p. Most modern SAT solvers accept SAT instances in CNF. For more details about SAT can be found elsewhere [1].
2.2 Periodic Event Scheduling Problem Let l, u ∈ Z and t ∈N. [l, u] := {x ∈ Z | l ≤ x ≤ u} denotes the interval from l to u and [l, u]t := z∈Z [l + z · t, u + z · t] ⊆ Z the interval from l to u modulo t,
Data Loading...
