2nd workshop of the Center of Modern Computer Science
2. seminář Centra moderní informatiky
The second workshop of the Center of Modern Computer Science will take place on Friday December 14, 2012.
Centrum moderní informatiky zve na druhý seminář, který se koná v rámci výročního workshopu Informatického ústavu UK a centra excelence Institut teoretické informatiky v pondělí 10. 12. s navazujícím vědeckým programem ve čtvrtek a pátek 13. a 14. 12. 2012. Přednášky juniorů centra se konají v pátek od 10:15, dále vystoupí řada hostů ze zahraničí i z domácích pracovišť. Všechny přednášky se konají v sále Bohuslava Martinů v budově HAMU, Malostranské nám. 13, Praha 1.
| 10:15 | Ondřej Pangrác: Coloring Eulerian triangulations of the Klein bottle |
|---|---|
| 10:40 | Petr Kučera: Propagation complete formulas |
| 11:05 | Pavel Surynek: Cooperative path finding for multiple robots |
Abstracts
Ondřej Pangrác: Coloring Eulerian triangulations of the Klein Bottle
(joint work with D. Kral, B. Mohar, A. Nakamoto, Y. Suzuki)
We prove that an Eulerian triangulation of the Klein bottle has chromatic number at most five unless it contains a complete graph of order six as a subgraph. As a consequence of our proof, we derive that every Eulerian triangulation of the Klein bottle with face-width at least four is 5-colorable.
Petr Kučera: Propagation Complete Formulas
(joint work with Martin Babka, Tomáš Balyo, Ondřej Čepek, Štefan Gurský and Václav Vlček)
The notion of propagation complete formulas was introduced in Knowledge compilation with empowerment. L. Bordeaux and J. Marques-Silva, SOFSEM 2012. A CNF formula F is propagation complete if after any partial substitution of truth values all logically entailed literals can be inferred from the resulting formula by unit propagation. The process which turns a CNF formula F into an equivalent propagation CNF formula F' is one of many ways of knowledge compilation. The key to this process is detecting the so called empowering implicates. Propagation complete formulas have connections to modern day SAT solvers based on CDCL (where the empowering implicates are used to enhance the original formula to make further search easier) and to CSP (where the CNF propagator for a constraint has to be propagation complete). In this talk we shall study several properties of propagation complete formulas with focus on complexity of the problems connected to this class of formulas. The main problems we study is how hard is to recognize whether given formula is propagation complete and how many implicates has to added to a formula to make it propagation complete. We also study the properties of empowering implicates some of which follow from the properties of modern day SAT solvers based on CDCL.
Pavel Surynek: Cooperative path finding for multiple robots
Consider a group of robots that are moving in a certain environment. Each robot is given its initial and goal location. The task of finding a sequence of moves for each robot such that it eventually reaches the given goal location by following this path is known as cooperative path finding (CPF). The interaction among robots is given by the requirement that they must not collide with each other. The CPF problem can be abstracted as a problem of motion on a graph where the graph represents the environment and robots are placed in vertices of the graph with at most one robot in a vertex. Complete and incomplete algorithms for solving the CPF problem and their properties will be discussed.
