Knowledge compilation for constraint programming
Public support
Provider
Ministry of Education, Youth and Sports
Programme
—
Call for proposals
—
Main participants
Univerzita Karlova / Matematicko-fyzikální fakulta
Contest type
M2 - International cooperation
Contract ID
MSMT-1907/2017
Alternative language
Project name in Czech
Kompilace znalostí pro programování s omezujícími podmínkami
Annotation in Czech
Cílem projektu je vyvinout nové techniky reformulace SAT a CSP problémů pro zvýšení efektivity jejich řešení případně garantování běhového času. Mezi hlavní cíle projektu patří: • Prozkoumání způsobů, jimiž by mohl být řešič splnitelnosti založený na CDCL upraven do podoby líného překladače, který umožní změnu vstupní formule v KNF do formule v KNF, která by byla úplná vzhledem k jednotkové propagaci. Tento líný překladač by byl jedním ze softwarových výstupů projektu. S konstrukcí překladače souvisí řada otevřených otázek, na které se plánujeme zaměřit. Vzhledem k tomu, že ověření toho, zda je vstupní formule v KNF úplná vzhledem k jednotkové propagaci, je coNP-úplným problémem, máme k dispozici polynomiální redukci na problém UNSAT (tedy problém, v němž se ptáme, zda daná formule je nesplnitelná). Naskýtá se zajímavá otázka, jak moc je tato redukce „praktická“, neboli jak výpočetně náročné by bylo praktické testování toho, zda je daná formule úplná vzhledem k jednotkové propagaci. Zodpovězení těchto otázek bude vyžadovat jak odvození nových teoretických výsledků, tak vytvoření potřebných programů a provedení řady experimentů. • Pro řadu specifických omezujících podmínek je naším cílem popsat taková kódování pomocí formule v KNF, pro něž je možno dosáhnout úplnosti vzhledem k jednotkové propagaci bez toho, aby bylo nutné přidávat exponenciálně mnoho klauzulí. Zde je naším cílem i prozkoumání vztahů mezi úplností těchto kódování vzhledem k jednotkové propagaci s různými formami konzistencí uvažovaných při programování s omezujícími podmínkami (doménová konzistence, konzistence okrajů, konzistence po cestě, ...) • Studium vlastností kompilace znalostí, kde výstupem je formule v KNF, pro různé vstupní formáty, identifikace vhodných strategií kódování pro tento způsob kompilace. Modelování problémů a reformulace modelů pro zvýšení efektivity jejich řešení v přímé návaznosti na aplikace jako je on-line konfigurace produktů, plánování a rozvrhování.
Scientific branches
R&D category
ZV - Basic research
CEP classification - main branch
IN - Informatics
CEP - secondary branch
—
CEP - another secondary branch
—
OECD FORD - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
This project was being realized in the framework of the MOBILITY Activity that aims primarily on establishing and strenghtening ties with foreign research institutions. The control of particular outputs is not implemented by the evalution committee, but the correctness of allocated finances and the adequacy of their use are checked.
Solution timeline
Realization period - beginning
Jan 1, 2017
Realization period - end
Dec 31, 2018
Project status
U - Finished project
Latest support payment
May 29, 2018
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP19-MSM-7A-U/01:1
Data delivery date
Jun 18, 2019
Finance
Total approved costs
108 thou. CZK
Public financial support
108 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK