ORGANIZATION

This symposium is jointly funded by the Wolfgang Pauli Institute and VCLA.

Symposium chairs:
Bart Selman (Cornell University)
Stefan Szeider (Vienna University of Technology)

AIMS AND SCOPE

Many fundamental computational problems that arise in various applications such as planning, scheduling, automated reasoning, or machine learning are theoretically intractable. In spite of their theoretical hardness, heuristic solvers are often able to solve large realistic problem instances surprisingly fast. For instance, the propositional satisfiability problem is NP-complete and it is believed that it cannot be solved in subexponential time. In contrast, today’s satisfiability solvers can handle routinely large real-world instances with hundreds of thousands of variables.

This discrepancy between theoretical hardness and practically solubility is often explained by the presence of a certain “hidden structure” in real-world instances. Apparently, heuristic solvers are able to exploit this hidden structure to solve the instances efficiently.

There are various approaches for identifying and studying hidden structure: among others, structure has been defined in terms of decomposability, in terms of the distance from some class of instances (backdoors), by measures that capture the small world phenomenon, or by proof complexity measures like resolution width or space. Some of these approaches are rigorous and theoretical, some are empirical. Some approaches give rise to qualitative notions of problem hardness or problem easiness.

The aim of this symposium is to bring together researchers from various disciplines who are concerned with hidden structure in problem instances. Lectures and discussions will put all these different approaches into context and will stimulate a fruitful exchange of ideas between different fields.

FORMAT

The symposium will feature invited talks and provide opportunities for all participants to engage in discussions on open problems and future directions.

Participation is by invitation only. Registration is free of charge and includes attendance to all symposium events and lectures, coffee breaks, and lunches.

The invited talks will be open to the public. Local people who are interested in some of the talks but do not want to participate in the entire symposium (and the social program) do not need to register.

INVITED SPEAKERS

Albert Atserias (Universitat Politècnica de Catalunya)
Armin Biere (Johannes Kepler University, Linz)
Rina Dechter (University of California, Irvine)
Serge Gaspers (NICTA and University of New South Wales, Sydney)
Georg Gottlob (Oxford University)
Holger Hoos (University of British Columbia)
Pete Jeavons (Oxford University)
Rolf Niedermeier (TU Berlin)
Jakob Nordström (KTH Royal Institute of Technology)
Jan Arne Telle (University of Bergen)
Toby Walsh (NICTA and University of New South Wales, Sydney)
Ryan Williams (Stanford)

DATE AND VENUE

May 16-18, 2013
Vienna University of Technology

Zemanek seminar room (location on ground floor)

Favoritenstraße 9-11 (Google Maps)
1040 Vienna, Austria

CO-LOCATED EVENT

Prof. Donald E. Knuth (Stanford) will give a lecture at the Vienna University of Technology on May 16th. Please follow this link for more information.

SCHEDULE

May 16th:

08:30-09:00 Registration
09:00-09:05 Welcome

09:05-10:05  Rolf Niedermeier
10:05-10:30  Coffee break
10:30-11:30   Ryan Williams
11:30-12:30   Serge Gaspers
12:30-14:00  Lunch break  (TU Mensa at Wiedner Hauptstraße 8-10, 1040 Vienna, vouchers will be available)
14:00-15:00  Toby Walsh
15:00-16:00  Holger Hoos
16:00-16:30  Coffee break

17:30 Prof. Knuth’s lecture (more information)

May 17th:

09:00 -10:00 Jakob Nordström
10:00-10:30  Coffee break
10:30-11:30   Albert Atserias
11:30-12:30    Pete Jeavons
12:30-14:00   Lunch break (Vouchers will be available for TU Mensa at Wiedner Hauptstraße 8-10, 1040 Vienna)
14:00-15:00   Georg Gottlob
15:00-16:00   Jan Arne Telle

18:30 Bus departure for restaurant Heuriger Werner Welser (click here for location)  from Favoritenstraße 12 (in front of Hotel Johann Strauß, directly opposite our computer science building)
19:00-21:30 Dinner
21:30 Bus departs for Favoritenstraße 12, 1040 Vienna

It is of course possible to take the public transport to our restaurant, so you will not depend on our rented bus.

May 18th:

09:30-10:30 Rina Dechter
10:30-11:30  Armin Biere

12:30 end of symposium, joint lunch (Restaurant Ischia, Mozartplatz 1, 1040 Vienna) until ~13:30

TALKS

• Albert Atserias: On the Proof-Search Problem for Resolution [abstract]
  Abstract.
  The proof-search problem for a propositional proof system P asks, for a given tautology as input, to find one of its P-proofs. It is known that finding the shortest resolution proof is an intractable problem. On the other hand the exact complexity of finding an approximately optimal resolution proof is much less understood. In this talk I will overview the status of this question. Along the way I will discuss how the industrially popular SAT-solvers that build on the methods of conflict-driven clause learning are able to solve the width-restricted proof-search problem for resolution, in near-optimal time.

• Armin Biere: Simulating Structual Reasoning on the CNF-Level [abstract]
  Abstract.

  In SAT solving finding the right encoding is a non-trivial task. Further, in many applications additional reasoning is performed outside the SAT solver, e.g. on the structural level. It is argued, that classical SAT solvers can not make use of certain structural knowledge, not available respectively hidden on the plain CNF-level. We first discuss important structural techniques used in combination with CNF-level SAT reasoning and then present algorithms, which allow to simulate some of these techniques on the CNF-level. Our motivation is not only to simplify practical applications of SAT solving, by moving more structural reasoning into the SAT solver, but particularly to improve its efficiency.

  Based on joined work with Marijn Heule (UT Texas) and Matti Järvisalo (Univ. Helsinki).

  [slides]

• Rina Dechter: Weighted ­­­AND/OR Multivalued Decision Diagrams (AOMDD) and the Semantic-Width [abstract]
  Abstract.

  Graphical models, e.g., Bayesian networks, Markov random fields, constraint networks and Influence diagrams, are widely applicable knowledge representation schemes that capture independencies in the knowledge base and support efficient, graph-based algorithms for a variety of reasoning tasks ranging from satisfiability, to combinatorial optimization to counting queries. 

  Answering queries over graphical models are known to be bounded exponentially in the graph treewidth thus tractable for bounded treewidth. Still, empirical experience on a range of tasks and benchmarks show that the treewidth bound is often extremely loose not only for satisfiability, but also for the more demanding tasks such as optimization and even counting. There is a need, therefore, in developing a more refined characteristic of problem instances that can capture better the instance-based complexity of the given problems.  One such measures may emerge from an alternative representation of a graphical model such as the weighted  AND/OR Multi-valued Decision Diagrams or, AOMDD.

  Weighted AOMDDs generalize Ordered Binary Decision Diagrams (OBDDs) in that they capture problem decomposition,  they accommodate multi-valued variables, and can express real-valued functions.  AOMDDs can be compiled from the graphical model specification, or may be learned and they are particularly suitable for domains involving mixed probabilistic and constrain-based information.

  In this talk I will present the weighted AND/OR Multi-valued decision diagrams (AOMDDs) and show that they can be viewed as search spaces whose traversal may yield an answer to a query.  The minimal, canonical,AOMDD provides a vivid display of the internal structure of the graphical model beyond the independencies that are specified in its input (primal) graph. We will show that for any ordering, the AOMDD size is bounded exponentially by the problem’s semantic-width, a new,  and more informative parameter (albeit hard to compute)  and will relate it  to the  AOMDD-width which is more computable. Specific demonstration as well as empirical evaluation will be provided as time permits.

  Collaborators: Robert Mateescu, Radu Marinescu, William Lam

  [slides]

• Serge Gaspers: Backdoors to Satisfaction: Parameterized Complexity [abstract]
  Abstract.

  A backdoor set is a set of variables of a propositional formula such that fixing the truth values of the variables in the backdoor set moves the formula into some class where the Satisfiability problem is polynomial-time decidable. If we know a small backdoor set we can reduce the question of whether the given formula is satisfiable to the same question for one or several easy formulas that belong to the tractable class under consideration. In this talk I will review parameterized complexity results for problems that arise in the context of backdoor sets, such as the problem of finding a backdoor set of size at most k, parameterized by k. I will also present an outline of a recent FPT-approximation algorithm finding a backdoor to the class of formulas with bounded incidence treewidth.

  Joint work with Stefan Szeider.

  [slides]

• Georg Gottlob: Robust Constraint Satisfaction and Local Hidden Variables in Quantum Mechanics [abstract]
  Abstract.

  Motivated by considerations in quantum mechanics, we introduce the class of robust constraint satisfaction problems in which the question is whether every partial assignment of a certain length can be extended to a solution, provided the partial assignment does not violate any of the constraints of the given instance. We explore the complexity of specific robust colorability and robust satisfiability problems, and show that they are NP-complete. We then use these results to establish the computational intractability of detecting local hidden-variable models in quantum mechanics.

  Joint work with Samson Abramsky and Phokion Kolaitis.

• Holger Hoos: Structure at the meta-level: Observations on the structure of design spaces of high-performance solvers for hard combinatorial problems [abstract]
  Abstract.

  Highly effective solvers for hard-combinatorial problems are typically the result of searching within large spaces of possible combinations of heuristic design choices. This search process has traditionally been carried out manually, guided by the intuitions of the solver designer and limited experimentation, but is now becoming increasingly automated. Clearly, the difficulty of this optimisation process depends heavily on the structure of the design space within which it takes place. In this talk, I will share some insights and speculation concerning the properties of those design spaces; in particular, I will attempt to shed some light on the reasons why automated design optimisation, carried out using state-of-the-art algorithm configuration procedures, is feasible in practice, despite the high cost of evaluating designs. I will also give some background on algorithm configuration procedures and explain why I believe these will play a key role not only in the design of effective solvers for hard combinatorial problems, but also in future investigations of the empirical complexity of those problems.

  [slides]

• Pete Jeavons: Structure in CSP and SAT: A case study [abstract]
  Abstract.

  Many features of a constraint satisfaction problem that are sufficient to make it tractable have been identified in theory, but are generally not exploited by current constraint-solving software. Such features may be lost or disguised when the problem is encoded as a SAT instance. However, SAT-solvers still do remarkably well in solving many kinds of problems in practice, and sometimes seem to be able to exploit their structure even when it is hidden. In this talk we will focus on a particular simple family of problems where SAT-solvers are much more effective than most CP solvers, and explain why this happens.

  Joint work with Justyna Petke.

  [slides]

• Rolf Niedermeier: On Multivariate Algorithmics and Structure Detection [abstract]
  Abstract.

  Multivariate algorithmics views NP-hard problems from multiple perspectives, depending on respectively chosen parameterizations. From a practical point view it is important to have parameters that adopt small values in real-world instances. Then, the goal is to prove (fixed-parameter) tractability in case of small parameter values, which, in particular, includes techniques for efficient and effective data reduction (kernelization).
  In this survey, we discuss several recent experiences with efforts towards a data-driven approach to identifying useful problem parameters. We present examples from various application domains, including network
  analysis, data anonymization, and computational social choice.

  [slides]

• Jakob Nordström: Relating Proof Complexity Measures and Practical Hardness of SAT [abstract]
  Abstract.

  Boolean satisfiability (SAT) solvers have improved enormously in performance over the last 10-15 years and are today an indispensable tool for solving a wide range of computational problems. However, our understanding of what makes SAT instances hard or easy in practice is still quite limited. A recent line of research in proof complexity has studied theoretical complexity measures such as length, width, and space in resolution, which is a proof system closely related to state-of-the-art conflict-driven clause learning (CDCL) SAT solvers. Although it seems like a natural question whether these complexity measures could be relevant for understanding the practical hardness of SAT instances, to date there has been very limited research on such possible connections.
  This work sets out on a systematic study of the interconnections between theoretical complexity and practical SAT solver performance. Our main focus is on space complexity in resolution, and we report results from extensive experiments aimed at understanding to what extent this measure is correlated with hardness in practice. Our conclusion from the empirical data is that the resolution space complexity of a formula would seem to be a more fine-grained indicator of whether the formula is hard or easy than the length or width needed in a resolution proof. On the theory side, we prove a separation of general and tree-like resolution space, where the latter has been proposed before as a measure of practical hardness, and also show connections between resolution space and backdoor sets.

  Joint work with Matti Jarvisalo, Massimo Lauria, Arie Matsliah, Marc Vinyals, and Stanislav Zivny.

  [slides]

• Jan Arne Telle: Dynamic programming on dense graphs [abstract]
  Abstract.

  Many NP-hard graph problems are tractable on restricted inputs, both for sparse graphs like trees and possibly dense graphs like interval graphs. The treewidth of a graph measures how close the graph is to being a tree and parameterizing by treewidth we get fixed parameter tractable (FPT) algorithms for many problems. Boolean-width is a recently introduced graph parameter motivated by clique-width, which can give FPT algorithms also on dense graphs. For example, any interval graph or permutation graph has boolean-width $O(\log n)$ and a random graph will almost surely have boolean-width $O(\log^{^2} n)$. In this talk we report on computational experiments with boolean-width, including a heuristic for finding decompositions of low boolean-width, and dynamic programming along the decomposition for solving a class of optimization problems.

• Toby Walsh: Detecting and Exploiting Subproblem Tractability / Global Scheduling Constraints under Structural Restrictions [abstract]
  Abstract.
  Detecting and Exploiting Subproblem Tractability

  Constraint satisfaction problems may be nearly tractable. For instance, most of the relations in a problem might belong to a tractable language. We introduce a method to take advantage of this fact by computing a backdoor to this tractable language. The method can be applied to many tractable classes for which the membership test is itself tractable. We introduce therefore two polynomial membership testing algorithms, to check if a language is closed under a majority or conservative Mal’tsev polymorphism, respectively. Then we show that computing a minimal backdoor for such classes is fixed parameter tractable (FPT) if the tractable subset of relations is given, and W[2]-complete otherwise. Finally, we report experimental results on the XCSP benchmark set. We identified a few promising problem classes where problems were nearly closed under a majority polymorphism and small backdoors could be computed.

  Joint work with Christian Bessiere, Clement Carbonnel, Emmanuel Hebrard and George Katsirelos.

  Global Scheduling Constraints under Structural Restrictions

  CUMULATIVE and INTERDISTANCE are key global constraints used in the modeling and solving scheduling problems. Enforcing domain consistency on both is NP-hard. However, restricted versions of these constraints are often sufficient in practice. Some examples include scheduling problems with a large number of similar tasks, or tasks sparsely distributed over time. Another example is runway sequencing problems in air-traffic control, where landing periods have a regular pattern. Such cases can be characterized in terms of structural restrictions on the constraints. We identify a number of such structural restrictions and investigate how they impact the computational complexity of propagating these global constraints. In particular, we prove that such restrictions often make propagation tractable.

  Joint work with Geoffrey Chu, Serge Gaspers, Nina Narodytska and Andreas Schutt.

  [slides: scheduling] [slides: subproblem]

• Ryan Williams: Substructure in SAT [abstract]
  Abstract.
  Ten years ago, Carla Gomes, Bart Selman, and I proposed the notion of “backdoor sets” to study what makes real-world SAT instances tractable in practice. The high-level idea is that many SAT instances from the real-world possess only a small number of variables that need to be determined — after that, the rest of the instance is “easy” to solve. I will give an overview of the definitions, the basic theorems about them, and some of the experimental work that has been done on the subject.
  [slides]

PARTICIPANTS

• Sebastian Arming (Vienna University of Technology)
• Albert Atserias (Universiat Politècnica de Catalunya)
• Adrian Balint (Ulm University)
• Armin Biere (Johannes Kepler University Linz)
• Simone Bova (Vienna University of Technology)
• Ronald de Haan (Vienna University of Technology)
• Rina Dechter (University of California, Irvine)
• Wolfgang Dvorák (University of Vienna)
• Johannes Fichte (Vienna University of Technology)
• Robert Ganian (Vienna University of Technology)
• Serge Gaspers (NICTA, U. of NS-Wales, Sydney)
• Georg Gottlob (Oxford University)
• Monika Henzinger (Universitaet Wien)
• Petr Hlinený (FI MU Brno)
• Holger Hoos (University of British Columbia)
• Markus Iser (Institute for Theoretical Informatics @KIT)
• Matti Järvisalo (University of Helsinki)
• Pete Jeavons (Oxford University)
• EunJung Kim (LAMSADE-Paris Dauphine)
• Donald Knuth (Stanford University)
• Mikko Koivisto (University of Helsinki)
• Martin Kronegger (Vienna University of Technology)
• O-joung Kwon (KAIST)
• Martin Lackner (Vienna University of Technology)
• Norbert Manthey (TU Dresden)
• Moritz Müller (Kurt Gödel Research Center, Wien)
• Nysret Musliu (Vienna University of Technology)
• Rolf Niedermeier (TU Berlin)
• Jakob Nordström (KTH Royal Institute of Technology)
• Sebastian Ordyniak (Vienna University of Technology)
• Sang-il Oum (KAIST)
• Daniel Paulusma (Durham University)
• Justyna Petke (University College London)
• Andreas Pfandler (Vienna University of Technology)
• Stefan Rümmele (TU Wien)
• Abdallah Saffidine (Lamsade, Université Paris-Dauphine)
• Bart Selman (Cornell University)
• Carsten Sinz (Karlsruhe Institute of Technology)
• Friedrich Slivovsky (Vienna University of Technology)
• Stefan Szeider (Vienna University of Technology)
• Jan Arne Telle (University of Bergen)
• Toby Walsh (NICTA, U. of NS-Wales, Sydney)
• Ryan Williams (Stanford)
• Stefan Woltran (Vienna University of Technology)
• Florian Zuleger (Vienna University of Technology)

PHOTOS

TRAVEL INFORMATION

Here are some suggestions for hotels close to the symposium venue:

Clima Cityhotel (www.climacity-hotel.com)

15 rooms available for special price (see below), book until 15.3.2013 via phone, fax or e-mail with the heading “Structure Workshop” (credit card number and expiration date needed for confirmation)

Single room: EUR 70 per night

Double room: EUR 80 per night

Phone: 0043 1 5051693

Fax: 0043 1 5043552

Email: moc.letoh-yticamilcnull@gnureivreser

Contact person: Ms Karina Gryska

Cancellation policy:

up to 8 weeks before arrival: no costs

up to 4 weeks before arrival: 60% of total room price

less than 4 weeks or no-show: 100% of total room price

Hotel Carlton Opera (www.carlton.at)

15 rooms available for special price (see below), book until 15.3.2013 via phone or e-mail with the heading “Structure Workshop” (credit card number and expiration date needed for confirmation)

Price EUR 79 per night

Phone: 0043 1 5875302

Email: ta.notlracnull@letoh

Contact person: Ms Doris Ferenczy

Cancellations: no costs until 1 day before arrival

Hotel Erzherzog Rainer (www.schick-hotels.com)

17 rooms available for special price (see below), book until 15.3.2013 via phone, fax or e-mail with the heading “Structure Workshop” (credit card number and expiration date needed for confirmation)

6 single rooms economy: EUR 89 per night

6 single rooms comfort: EUR 108 per night

5 double rooms: EUR 154 per night ( for single use: EUR 125 per night)

Phone: 0043 1 22111 316
Fax: 0043 1 22111 350
Email: moc.sletoh-kcihcsnull@reniar

Contact person: Ms Maria Leitgeb

Cancellation: no costs until 2 days before arrival

Hotel Europa (www.austria-trend.at)

40 rooms available, book until 30.4.2013, via phone, fax or e-mail with the heading “Structure Workshop” (credit card number and expiration date needed for confirmation)

Price: EUR 160 per night

Phone: 0043 1 5157788
Fax: 0043 1 5157782
Email: ta.dnert-airtsuanull@neiw.aporue.gnureivreser

Contact person: Ms Neriza Panek

Cancellations:
until21 before arrival: no costs
until 14 days before arrival: 50% of complete stay
until 7 days before arrival: 80% of complete stay
less than 7 days before arrival or no-show: 100% of complete stay

Hotel Astoria (www.austria-trend.at)

20 rooms available, book until 30.4.2013 via phone, fax or e-mail with the heading “Structure Workshop” (credit card number and expiration date needed for confirmation)

Price: EUR 170 per night

Phone: 0043 1 5157788
Fax: 0043 1 5157782
Email: ta.dnert-airtsuanull@airotsa.gnureivreser

Contact person: Frau Neriza Panek

Cancellations:
until21 before arrival: no costs
until 14 days before arrival: 50% of complete stay
until 7 days before arrival: 80% of complete stay
less than 7 days before arrival or no-show: 100% of complete stay

Wombats City Hostel (http://www.wombats-hostels.com)

If you are on a tight budget you might want to consider the following option:

Recently opened a city hostel Wombats, very close to the workshop venue. They offer double rooms for EUR 32, rooms shared by several people are even much cheaper. Please make sure to select “THE NASCHMARKT” as other branches of the hostel are located further away. We could not reserve rooms at the hostel, but if you book early, there should be rooms available.

For further information, please have a look at our visitors’ guide.