View: session overviewtalk overviewside by side with other conferences

08:45 | FLoC Plenary Talk: From Reachability to Temporal Specifications in Game Theory SPEAKER: Orna Kupfermann ABSTRACT. Multi-agents games are extensively used for modelling settings in which different entities share resources. For example, the setting in which entities need to route messages in a network is modelled by network-formation games: the network is modelled by a graph, and each agent has to select a path satisfying his reachability objective. In practice, the objectives of the entities are often more involved than reachability. The need to specify and reason about rich specifications has been extensively studied in the context of verification and synthesis of reactive systems. The talk describes a lifting of ideas from formal methods to multi-agent games. For example, in network-formation games with regular objectives, the edges of the graph are labeled by alphabet letters and the objective of each player is a regular language over the alphabet of labels. Thus, beyond reachability, a player may restrict attention to paths that satisfy certain properties, referring, for example, to the providers of the traversed edges, the actions associated with them, their quality of service, security, etc. The talk assumes no previous knowledge in game theory. We will introduce the basic concepts and problems, describe how their extension to games with more expressive specification of objectives poses new challenges, and study the resulting games. Joint work with Guy Avni and Tami Tamir. |

10:45 | Long Proofs of (Seemingly) Simple Formulas SPEAKER: Mladen Miksa ABSTRACT. In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for state-of-the-art SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become very easy). Somewhat intriguingly, however, the very hardest instances in practice seem to arise from so-called fixed bandwidth matrices, which are provably easy for resolution and are also simple in practice if the solver is given a hint about the right branching order to use. This would seem to suggest that CDCL with current heuristics does not always search efficiently for short resolution proofs, despite the theoretical results of [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte, and Thurley2011]. |

11:15 | Proof complexity and the Lovasz-Kneser Theorem SPEAKER: Adrian Crăciun ABSTRACT. We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the Kneser-Lovasz Theorem. This is a family of propositional tautologies, indexed by an nonnegative integer parameter k that generalizes the Pigeonhole Principle (PHP, obtained for k=1). We show for all fixed $k$ $2^{\Omega(n)}$ lower bounds on resolution complexity and exponential lower bounds for bounded depth Frege proofs. These results hold even for the more restricted class of formulas encoding Schrijver's strengthening of the Kneser-Lovasz Theorem. On the other hand for the cases $k=2,3$ (for which combinatorial proofs of the Kneser-Lovasz Theorem are known) we give polynomial size Frege (k=2), respectively extended Frege (k=3) proofs. The paper concludes with a brief discussion of the results (that will be presented in a subsequent paper) on the complexity of the general case of the Kneser-Lovasz theorem. |

14:30 | A (Biased) Proof Complexity Survey for SAT Practitioners SPEAKER: Jakob Nordström |

16:30 | QBF Resolution Systems and their Proof Complexities SPEAKER: Valeriy Balabanov ABSTRACT. Quantified Boolean formula (QBF) evaluation has a broad range of applications in computer science and is gaining increasing attention. Recent progress has shown that for a certain family of formulas Q-resolution, which forms the foundation of learning in modern search-based QBF solvers, is exponentially inferior in proof length to its extended variants: long-distance Q-resolution (LQ-resolution) and Q-resolution with resolution over universal literals (QU-resolution). The relative proof power between LQ-resolution and QU-resolution, however, remains unknown. In this paper, we show their incomparability by exponential separations on two families of QBFs, and further proposes a combination of the two resolution methods to achieve an even more powerful proof system. These results may shed light on solver development with enhanced learning mechanisms. In addition, we show how QBF Skolem/Herbrand certificate extraction can benefit from polynomial LQ-resolution proofs in contrast to their exponential Q-resolution counterparts. |

19:00 | VSL Public Lecture: Gödel in Vienna SPEAKER: Karl Sigmund |