Line planning, i.e. choosing routes which are to be serviced by vehicles in order to satisfy network demands, is an important aspect of public transport planning. While there exist heuristic procedures for generating lines from scratch, most theoretical investigations consider the problem of choosing lines only from a predefined line pool. We consider the line planning problem when all simple paths can be used as lines and present an algorithm which is fixed-parameter tractable, i.e. it is efficient on instances with small parameter. As a parameter we consider the treewidth of the public transport network, along with its maximum degree as well as the maximum allowed frequency.

This paper considers the length of resolution proofs when using Krishnamurthy's classic symmetry rules. We show that inconsistent linear equation systems of bounded width over a fixed finite field $\mathbb{F}_p$ with $p$ a prime have, in their standard encoding as CNFs, polynomial length resolutions when using the local symmetry rule (SRC-II). As a consequence it follows that the multipede instances for the graph isomorphism problem encoded as CNF formula have polynomial length resolution proofs. This contrasts exponential lower bounds for individualization-refinement algorithms on these graphs. For the Cai-Fürer-Immerman graphs, for which Torán showed exponential lower bounds for resolution proofs (SAT 2013), we also show that already the global symmetry rule (SRC-I) suffices to allow for polynomial length proofs.