7 papers
Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving
Haoze Wu, André Schidler, Armin Biere +1
Modern SAT solvers combine a rich repertoire of proof rules with sophisticated strategies that determine when and how to apply them. Often, the internal implementations are tightly…
Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach
Hannes Ihalainen, Dieter Vandesande, André Schidler +3
The implicit hitting set (IHS) approach offers a general framework for solving computationally hard combinatorial optimization problems declaratively. IHS iterates between a decisi…
A Dynamic MaxSAT-based Approach to Directed Feedback Vertex Sets
Rafael Kiesel, André Schidler
We propose a new approach to the Directed Feedback Vertex Set Problem (DFVSP), where the input is a directed graph and the solution is a minimum set of vertices whose removal makes…
Weighted Model Counting with Twin-Width
Robert Ganian, Filip Pokrývka, André Schidler +2
Bonnet et al. (FOCS 2020) introduced the graph invariant twin-width and showed that many NP-hard problems are tractable for graphs of bounded twin-width, generalizing similar resul…
A SAT Approach to Twin-Width
André Schidler, Stefan Szeider
The graph invariant twin-width was recently introduced by Bonnet, Kim, Thomassé, and Watrigan. Problems expressible in first-order logic, which includes many prominent NP-hard prob…
Solving the Steiner Tree Problem with few Terminals
Johannes K. Fichte, Markus Hecher, Andre Schidler
The Steiner tree problem is a well-known problem in network design, routing, and VLSI design. Given a graph, edge costs, and a set of dedicated vertices (terminals), the Steiner tr…