24th Estonian Winter School in Computer Science (EWSCS)
XXIV Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 3 - 8, 2019

Student Talks 2019 (abstracts)

On Tseitin formulas, read-once branching programs and treewidth

Ludmila Glinskih
St. Petersburg Department of
V. A. Steklov Institute of Mathematics, Russian Federation

In this talk, we present a proof that any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on an ntimes n grid graph has size at least 2Ω(n). Then using the Excluded Grid Theorem of Robertson and Seymour we show that for an arbitrary graph G = (V,E) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on G has size at least 2Ω(tw(G)δ) for all δ < 1/36, where tw(G) is the treewidth of G. We will also show an upper bound O(|E| 2pw(G)), where pw(G) is the pathwidth of G.

This is joint work with Dmitry Itsykson.

Lower bounds on the Ordering and Dense Linear Ordering principles with splitting by linear equations

Sviatoslav Griaznov
St. Petersburg Department of
V. A. Steklov Institute of Mathematics, Russian Federation

We consider the proof system Res(+) introduced by Itsykson and Sokolov, which is an extension of Resolution proof system and operates with disjunctions of linear equations over F_2. We construct a framework based on Prover-Delayer games for proving lower bounds on tree-like Res(+) refutations for families on unsatisfiable CNF-formulas with certain properties. The framework generalizes the ideas used for proving exponential lower bound on Pigeonhole principle. Then we use this method to prove exponential lower bounds on tree-like Res(+) refutations for the Ordering and Dense Linear Ordering principles by Prover-Delayer games.

The Ordering principle states that there are no linear orderings without minimum. We give 2n−O(1) lower bound on the size of any tree-like Res(+) refutation. It is also possible to prove the similar but slightly worse lower bound 2n/4−O(1) using the lower bound on the degree of the derivation in Polynomial Calculus of Graph-Ordering principle.

The Dense Linear Ordering principle states that there are no dense linear orderings. We give 2n/3−O(1) lower bound on the size of any tree-like Res(+) refutation. This principle was considered by Atserias and Dalmau. There are no known lower bounds in Polynomial Calculus on graph variants of this principle (unlike the case of Graph-Ordering). This proof is more involved than the proof for Ordering principle; it uses ideas from both the Ordering principle’s lower bound proof and the Pigeonhole principle’s lower bound proof.

Both the Ordering and Dense Linear Ordering principles have Resolution refutations of polynomial size. Thus we give natural examples that are hard for tree-like Res(+) and easy for Resolution.

In addition, Itsykson and Knop described how to construct a hard satisfiable formulas for drunken DPLL(+) algorithms based on hard unsatisfiable formulas such that their hardness is proved by Prover-Delayer games. Thus this examples can be used to construct hard satisfiable formulas for drunken DPLL(+) algorithms.

This is work submitted to CSR 2019.

From the UNIX diff to structural diffing: the pitfalls!

Victor Miraldo
University of Utrecht, Netherlands

The UNIX diff is the de facto standard in computing the differences between two source files in a version control system. It does so by comparing the two files line-by-line. Extending the UNIX diff algorithm to compare the files by their abstract syntax trees is a computationally expensive process and has a number of pitfalls. In this short talk we go over a theoretical pitfall that gives rise to the computational inefficiency.

Correctness of compilation from WeakestMO to IMM weak memory model

Evgenii Moiseenko
St. Petersburg State University
Fac. of Math. and Mechanics, Russian Federation

The problem of giving a formal semantics for weak memory model of a high-level programming languages is known to be challenging. Recently, Chakraborty & Vafeiadis proposed a new solution to this problem. Their model, called WeakestMO, is based on event structures. Our work is dedicated to the mechanization of this model in the Coq theorem prover. In particular we want to prove a correctness of compilation from WeakestMO to IMM (intermediate memory model), that is a memory model that abstracts over modern hardware memory models.

Bridging the gap between programming languages and hardware weak memory models

Anton Podkopaev
St. Petersburg Higher School of Economics
and JetBrains Research, Russian Federation

We develop a new intermediate weak memory model, IMM, as a way of modularizing the proofs of correctness of compilation from concurrent programming languages with weak memory consistency semantics to mainstream multi-core architectures, such as POWER and ARM. We use IMM to prove the correctness of compilation from the promising semantics of Kang et al. to POWER (thereby correcting and improving their result) and ARMv7, as well as to the recently revised ARMv8 model. Our results are mechanized in Coq, and to the best of our knowledge, these are the first machine-verified compilation correctness results for models that are weaker than x86-TSO.

This is joint work with Ori Lahav and Viktor Vafeiadis. It appeared in POPL '19.

Lower bounds for 1-NBP calculus

Artur Riazanov
St. Petersburg Academic University
Dept. of Math. and IT, Russian Federation

We consider a semantic extension of OBDD-based proof systems operating with nondeterministic read-once branching programs. A refutation of a CNF formula φ in 1-NBP(AND, exists)-calculus is a sequence of nondeterministic read-once branching programs D1, D2, ..., Ds such that for every i, Di either represents a clause of φ or represents the conjunction of two 1-NBPs with smaller numbers, or Di = exists x Dj for j < i, where x is a propositional variable, and Ds represents the identically false function. We say that a 1-NBP(AND, exists)-refutation is an 1-NBP(AND, &exists;k) refutation if the set of variables that are used for the projection rule has size at most k. We show that there exists a constant C such that for every n there exists an explicit constant degree-graph G with n vertices such that every 1-NBP(AND, existsCn) refutation of a Tseitin formula based on G has size at least 2Ω(n).

During the talk I will focus on the transition between the lower bound for 1-NBP(AND) and the lower bound for 1-NBP(AND, existsCn).

This is based on joint work with Sam Buss, Dmitry Itsykson, Aleksandr Knop and Dmitry Sokolov.

Towards cost-utility quantile analysis of thermal-aware spatial scheduling for multi-cores

Muhammad Usama Sardar
Technische Universität Dresden, Germany

The increasing usage of multi-cores in safety-critical applications, such as aerospace, demands high levels of reliability, which exponentially depends on the on-chip temperature. The spatial scheduling of tasks is one of the key factors which determine the resulting core temperatures. However, commonly used techniques, such as simulation based on benchmarks, often miss critical bugs which result in catastrophic failures. Traditional model checking, on the other hand, has the inability to model the randomized aspects of scheduling, such as the arrival of tasks. In order to overcome these limitations, we propose to use probabilistic model checking for the cost-utility quantile analysis to provide probabilistic guarantees in accordance with the criticality of the system. Specifically, we present an improved formal thermal model for multi-cores incorporating transient temperatures and thermal coupling effects among the cores. Based on the proposed thermal model, we analyze two of the most urgent thermal management problems in multi-cores, and present a methodology for the formal comparative analysis of heuristics for thermal-aware spatial scheduling.

This is joint work with Clemens Dubslaff, Sascha Kluppelholz, Akash Kumar, Christel Baier.

Complexity of read-once branching programs for satisfiable and unsatisfiable Tseitin formulas

Petr Smirnov
St. Petersburg State University
Fac. of Math. and Mechanics, Russian Federation

We study the read-once branching program (1-BP) complexity of two natural problems based on Tseitin formulas. We show that the complexity of evaluation of a satisfiable Tseitin formula based on a graph G and the complexity of finding a vertex with violated parity condition for an unsatisfiable Tseitin formula based on the same graph G are quasipolynomially related for read-once branching programs.

Let S be the minimal size of 1-BP for the vertex search problem based on graph G. We show that the minimal size of a 1-BP computing the value of a satisfiable Tseitin formula based on the same graph G is at least S/n and at most SO(log n), where n is the number of vertices in the graph. We also show that if Ts(G, c) is a CNF encoding of an unsatisfiable Tseitin formula based on G, then the negation of Ts(G, c) has a constant-depth Frege proof of size O(S*|Ts(G, c)|4).

This is joint work with Ludmila Glinskih, Dmitry Itsykson, Artur Riazanov, submitted to ICALP 2019.

Valid CSS! Valid XHTML 1.0 Strict Last changed November 26, 2014 19:55 Europe/Helsinki (GMT +02:00) by local organizers, ewscs19(at)cs.ioc.ee
EWSCS'19 page: http://cs.ioc.ee/ewscs/2019/