Knowledge compilation languages as proof systems
In this paper, we study proof systems in the sense of Cook-Reckhow for problems that are higher in the polynomial hierarchy than coNP, in particular, #SAT and maxSAT. We start by explaining how the notion of Cook-Reckhow proof systems can be apply to these problems and show how one can twist existing languages in knowledge compilation such as decision DNNF so that they can be seen as proof systems for problems such as #SAT and maxSAT.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
A Knowledge Compilation Map
We propose a perspective on knowledge compilation which calls for analyzing different compilation approaches according to two key dimensions: the succinctness of the target compilation language, and the class of queries …
Beyond the C: Retargetable Decompilation using Neural Machine Translation
The problem of reversing the compilation process, decompilation, is an important tool in reverse engineering of computer software. Recently, researchers have proposed using techniques from neural machine translation to a…
C++ codeMachine TranslationTranslationLower Bounds for Approximate Knowledge Compilation
Knowledge compilation studies the trade-off between succinctness and efficiency of different representation languages. For many languages, there are known strong lower bounds on the representation size, but recent work s…
NegationOn the Role of Canonicity in Bottom-up Knowledge Compilation
We consider the problem of bottom-up compilation of knowledge bases, which is usually predicated on the existence of a polytime function for combining compilations using Boolean operators (usually called an Apply functio…
Open-Ended Question AnsweringEfficient Explanations for Knowledge Compilation Languages
Knowledge compilation (KC) languages find a growing number of practical uses, including in Constraint Programming (CP) and in Machine Learning (ML). In most applications, one natural question is how to explain the decisi…
Negation