Boolean Representation Languages Complete for Unit Propagation
Project goals
This is a basic research project in which we plan to work on problems in the area of knowledge compilation. We consider a particular case of knowledge compilation where the knowledge base is represented by a boolean function, usually in a conjunctive normal form (CNF) formula. We plan to study a compilation of such a formula into another CNF formula which is complete for unit propagation. More precisely, we will consider compilation into the target language of unit refutation complete formulas (URC), the language of propagation complete formulas (PC), and the corresponding variants of encodings with auxiliary variables, namely URC and PC encodings. The goal of this project is to solve theoretical questions related to compilation into URC or PC representation or encoding and develop a compiler for this task. To this end we shall develop and test algorithms and heuristic for automatic compilation. The outputs of this project will be published in journal and conference papers.
Keywords
boolean representation languagesunit propagation completenessknowledge compilationconstraint encodingSATsolvers
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 23 (SGA0201900001)
Main participants
Univerzita Karlova / Matematicko-fyzikální fakulta
Contest type
VS - Public tender
Contract ID
19-19463S
Alternative language
Project name in Czech
Reprezentace booleovských funkcí úplné vzhledem k jednotkové propagaci
Annotation in Czech
Jde o projekt základního výzkumu, v němž plánujeme pracovat na problémech z oblasti kompilace znalostí. Uvažujeme speciální případ kompilace znalostí, kde znalostní báze je reprezentovaná booleovskou funkcí, obvykle reprezentovanou formulí v konjunktivní normální formě (KNF). Plánujeme studium takové kompilace, kde je formule upravována do jiné KNF formule, jež je úplná vzhledem k jednotkové propagaci. Přesněji, budeme uvažovat situaci, kde cílovým jazykem kompilace je jazyk formulí úplných vzhledem k zamítání pomocí jednotkové propagace (unit refutation complete, URC) a jazyk formulí úplných vzhledem k odvozování literálů pomocí jednotkové propagace (propagation complete, PC). Cílem projektu je řešení teoretických otázek souvisejících s kompilací do URC nebo PC reprezentace či kódování a vývoj kompilátoru pro tuto úlohu. Za tím účelem budeme navrhovat a testovat algoritmy a heuristiky pro automatickou kompilaci. Výstupy projektu budou publikovány formou článků ve vědeckých časopisech a konferenčních sbornících.
Scientific branches
R&D category
ZV - Basic research
OECD FORD - main branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - secondary branch
—
OECD FORD - another secondary branch
—
AF - Documentation, librarianship, work with information
BC - Theory and management systems
BD - Information theory
IN - Informatics
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
While not completing all objectives to full extent, the project made substantial contributions in the planned directions and its scientific contribution is satisfactory. No issues with regards to fund spending were raised.
Solution timeline
Realization period - beginning
Jan 1, 2019
Realization period - end
Jun 30, 2022
Project status
U - Finished project
Latest support payment
Apr 1, 2022
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
CEP23-GA0-GA-U
Data delivery date
Jun 26, 2023
Finance
Total approved costs
6,019 thou. CZK
Public financial support
4,789 thou. CZK
Other public sources
1,230 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
6 019 CZK thou.
Public support
4 789 CZK thou.
79%
Provider
Czech Science Foundation
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Solution period
01. 01. 2019 - 30. 06. 2022