Kompilace znalostí pro programování s omezujícími podmínkami

Poskytovatel

Ministerstvo školství, mládeže a tělovýchovy

Program

Šestý rámcový program Evropského společenství pro výzkum, technický rozvoj a demonstrační činnosti

Veřejná soutěž

—

Hlavní účastníci

Univerzita Karlova / Matematicko-fyzikální fakulta

Druh soutěže

M2 - Mezinárodní spolupráce

Číslo smlouvy

MSMT-1907/2017

Název projektu anglicky

Knowledge compilation for constraint programming

Anotace anglicky

The principal aim of the research project is to develop new techniques for SAT and CSP reformulations which improve the effectivity of problem solving or bring guarantees for the running time. The main objectives of the project include: • Determining how a CDCL SAT solver can be modified into a lazy compiler, enabling to turn an input CNF into a propagation complete one. Such a lazy compiler would be one of the software outputs of the project. There are many open questions related to this task. Since checking if an input formula in CNF is propagation complete is a coNP-complete problem we have a polynomial reduction of this problem to UNSAT (a problem where we ask if a given formula is unsatisfiable). An interesting question arises how this reduction would be „practical“, that is how computationally demanding it would be to practically test if a formula is propagation complete. Answering these and other related questions will require us to derive new theoretical results, produce necessary programs, and perform series of experiments. • Describing new encodings of a number of specific global constraints. We are particularly interested in designing such encodings which do not require adding an exponential number of clauses to make them propagation complete. We aim to study relations of propagation completeness of these encodings with various types of consistencies in CSP (domain consistency, bound consistency, path consistency, …). • Studying properties of knowledge compilation where the output is in a form of a CNF for various kinds of input representations. We want to identify suitable strategies of encoding for this kind of compilation. We also want to study modelling problems and model reformulations, where our goal is to increase the effectivity of the solving process for such models, especially those dealing with applications such as on-line product configuration, planning, and scheduling.

Kategorie VaV

ZV - Základní výzkum

CEP - hlavní obor

IN - Informatika

CEP - vedlejší obor

—

CEP - další vedlejší obor

—

OECD FORD - odpovídající obory <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Hodnocení poskytovatelem

U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)

Zhodnocení výsledků projektu

Projekt byl realizován v rámci Aktivity MOBILITY, jejímž hlavním cílem je navázání a prohlubování kontaktů se zahraničními výzkumnými institucemi. Neprobíhá tedy kontrola dílčích výstupů projektu prostřednictvím hodnotící komise, avšak je kontrolována správnost čerpání přidělených financí a přiměřenost jejich využití.

Zahájení řešení

1. 1. 2017

Ukončení řešení

31. 12. 2018

Poslední stav řešení

U - Ukončený projekt

Poslední uvolnění podpory

29. 5. 2018

Důvěrnost údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Systémové označení dodávky dat

CEP19-MSM-7A-U/01:1

Datum dodání záznamu

18. 6. 2019

Celkové uznané náklady

108 tis. Kč

Výše podpory ze státního rozpočtu

108 tis. Kč

Ostatní veřejné zdroje financování

0 tis. Kč

Neveřejné tuz. a zahr. zdroje finan.

0 tis. Kč