arXiv subjects

Petr Kučera

Publications and source records attributed to Petr Kučera.

10 recordsLinked to original sources

arXiv2026

Parameterized Complexity Of Representing Models Of MSO Formulas

Monadic second order logic (MSO2) plays an important role in parameterized complexity due to the Courcelle's theorem. This theorem states that the problem of checking if a given graph has a property specified by a given MSO2 formula can be solved by a parameterized linear time algorithm with respect to the treewidth of the graph and the size of the formula. We extend this result by showing that models of MSO2 formula with free variables can be represented with a decision diagram whose size is parameterized linear in the above mentioned parameter. In particular, we show a parameterized linear upper bound on the size of a sentential decision diagram (SDD) when treewidth is considered and a parameterized linear upper bound on the size of an ordered binary decision diagram (OBDD) when considering the pathwidth in the parameter. In addition, building on a lower bound on the size of OBDD by Razgon (2014), we show that there is an MSO2 formula and a class of graphs with bounded treewidth which do not admit an OBDD with the size parameterized by the treewidth. Our result offers a new perspective on the Courcelle's theorem and connects it to the area of knowledge representation.

cs.AI↗

arXiv2021

Propagation complete encodings of smooth DNNF theories

We investigate conjunctive normal form (CNF) encodings of a function represented with a decomposable negation normal form (DNNF). Several encodings of DNNFs and decision diagrams were considered by (Abio et al. 2016). The authors differentiate between encodings which implement consistency or domain consistency by unit propagation from encodings which are unit refutation complete or propagation complete. The difference is that in the former case we do not care about propagation strength of the encoding with respect to the auxiliary variables while in the latter case we treat all variables (the main and the auxiliary ones) in the same way. The currently known encodings of DNNF theories implement domain consistency. Building on these encodings we generalize the result of (Abio et al. 2016) on a propagation complete encoding of decision diagrams and present a propagation complete encoding of a DNNF and its generalization for variables with finite domains.

cs.AI↗

arXiv2021

Backdoor Decomposable Monotone Circuits and their Propagation Complete Encodings

We describe a compilation language of backdoor decomposable monotone circuits (BDMCs) which generalizes several concepts appearing in the literature, e.g. DNNFs and backdoor trees. A $\mathcal{C}$-BDMC sentence is a monotone circuit which satisfies decomposability property (such as in DNNF) in which the inputs (or leaves) are associated with CNF encodings from a given base class $\mathcal{C}$. We consider the class of propagation complete (PC) encodings as a base class and we show that PC-BDMCs are polynomially equivalent to PC encodings. Additionally, we use this to determine the properties of PC-BDMCs and PC encodings with respect to the knowledge compilation map including the list of efficient operations on the languages.

cs.AI↗

arXiv2020

Bounds on the size of PC and URC formulas

In this paper we investigate CNF formulas, for which the unit propagation is strong enough to derive a contradiction if the formula together with a partial assignment of the variables is unsatisfiable (unit refutation complete or URC formulas) or additionally to derive all implied literals if the formula is satisfiable (propagation complete or PC formulas). If a formula represents a function using existentially quantified auxiliary variables, it is called an encoding of the function. We prove several results on the sizes of PC and URC formulas and encodings. One of them are separations between the sizes of formulas of different types. Namely, we prove an exponential separation between the size of URC formulas and PC formulas and between the size of PC encodings using auxiliary variables and URC formulas. Besides of this, we prove that the sizes of any two irredundant PC formulas for the same function differ at most by a factor polynomial in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.

cs.LO↗

arXiv2020

Generating clause sequences of a CNF formula

Given a CNF formula $Φ$ with clauses $C_1,\ldots,C_m$ and variables $V=\{x_1,\ldots,x_n\}$, a truth assignment $a:V\rightarrow\{0,1\}$ of $Φ$ leads to a clause sequence $σ_Φ(a)=(C_1(a),\ldots,C_m(a))\in\{0,1\}^m$ where $C_i(a) = 1$ if clause $C_i$ evaluates to $1$ under assignment $a$, otherwise $C_i(a) = 0$. The set of all possible clause sequences carries a lot of information on the formula, e.g. SAT, MAX-SAT and MIN-SAT can be encoded in terms of finding a clause sequence with extremal properties. We consider a problem posed at Dagstuhl Seminar 19211 "Enumeration in Data Management" (2019) about the generation of all possible clause sequences of a given CNF with bounded dimension. We prove that the problem can be solved in incremental polynomial time. We further give an algorithm with polynomial delay for the class of tractable CNF formulas. We also consider the generation of maximal and minimal clause sequences, and show that generating maximal clause sequences is NP-hard, while minimal clause sequences can be generated with polynomial delay.

cs.DM↗

arXiv2020

Unique key Horn functions

Given a relational database, a key is a set of attributes such that a value assignment to this set uniquely determines the values of all other attributes. The database uniquely defines a pure Horn function $h$, representing the functional dependencies. If the knowledge of the attribute values in set $A$ determines the value for attribute $v$, then $A\rightarrow v$ is an implicate of $h$. If $K$ is a key of the database, then $K\rightarrow v$ is an implicate of $h$ for all attributes $v$. Keys of small sizes play a crucial role in various problems. We present structural and complexity results on the set of minimal keys of pure Horn functions. We characterize Sperner hypergraphs for which there is a unique pure Horn function with the given hypergraph as the set of minimal keys. Furthermore, we show that recognizing such hypergraphs is co-NP-complete already when every hyperedge has size two. On the positive side, we identify several classes of graphs for which the recognition problem can be decided in polynomial time. We also present an algorithm that generates the minimal keys of a pure Horn function with polynomial delay. By establishing a connection between keys and target sets, our approach can be used to generate all minimal target sets with polynomial delay when the thresholds are bounded by a constant. As a byproduct, our proof shows that the Minimum Key problem is at least as hard as the Minimum Target Set Selection problem with bounded thresholds.

cs.DM↗

arXiv2019

Approximating minimum representations of key Horn functions

Horn functions form a subclass of Boolean functions and appear in many different areas of computer science and mathematics as a general tool to describe implications and dependencies. Finding minimum sized representations for such functions with respect to most commonly used measures is a computationally hard problem that remains hard even for the important subclass of key Horn functions. In this paper we provide logarithmic factor approximation algorithms for key Horn functions with respect to all measures studied in the literature for which the problem is known to be hard.

cs.DS↗

arXiv2018

Phase Transition in Matched Formulas and a Heuristic for Biclique Satisfiability

A matched formula is a CNF formula whose incidence graph admits a matching which matches a distinct variable to every clause. We study phase transition in a context of matched formulas and their generalization of biclique satisfiable formulas. We have performed experiments to find a phase transition of property "being matched" with respect to the ratio $m/n$ where $m$ is the number of clauses and $n$ is the number of variables of the input formula $φ$. We compare the results of experiments to a theoretical lower bound which was shown by Franco and Gelder (2003). Any matched formula is satisfiable, moreover, it remains satisfiable even if we change polarities of any literal occurrences. Szeider (2005) generalized matched formulas into two classes having the same property -- var-satisfiable and biclique satisfiable formulas. A formula is biclique satisfiable if its incidence graph admits covering by pairwise disjoint bounded bicliques. Recognizing if a formula is biclique satisfiable is NP-complete. In this paper we describe a heuristic algorithm for recognizing whether a formula is biclique satisfiable and we evaluate it by experiments on random formulas. We also describe an encoding of the problem of checking whether a formula is biclique satisfiable into SAT and we use it to evaluate the performance of our heuristic

cs.DS↗

arXiv2018

A lower bound on CNF encodings of the at-most-one constraint

Constraint "at most one" is a basic cardinality constraint which requires that at most one of its $n$ boolean inputs is set to $1$. This constraint is widely used when translating a problem into a conjunctive normal form (CNF) and we investigate its CNF encodings suitable for this purpose. An encoding differs from a CNF representation of a function in that it can use auxiliary variables. We are especially interested in propagation complete encodings which have the property that unit propagation is strong enough to enforce consistency on input variables. We show a lower bound on the number of clauses in any propagation complete encoding of the "at most one" constraint. The lower bound almost matches the size of the best known encodings. We also study an important case of 2-CNF encodings where we show a slightly better lower bound. The lower bound holds also for a related "exactly one" constraint.

cs.CC↗

arXiv2014

Solutions to the Navier-Stokes Equations with Mixed Boundary Conditions in Two-Dimensional Bounded Domains

In this paper we consider the system of the non-steady Navier-Stokes equations with mixed boundary conditions. We study the existence and uniqueness of a solution of this system. We define Banach spaces $X$ and $Y$, respectively, to be the space of "possible" solutions of this problem and the space of its data. We define the operator $\mathcal{N}:X\rightarrow Y$ and formulate our problem in terms of operator equations. Let $\mathbf{u}\in X$ and ${{\mathcal G}_{\mathcal P}}_{\mathbf{u}}: X\rightarrow Y$ be the Frechet derivative of $\mathcal{N}$ at $\mathbf{u}$. We prove that ${{\mathcal G}_{\mathcal P}}_{\mathbf{u}}$ is one-to-one and onto $Y$. Consequently, suppose that the system is solvable with some given data (the initial velocity and the right hand side). Then there exists a unique solution of this system for data which are small perturbations of the previous ones. Next result proved in the Appendix of this paper is $W^{2,2}$- regularity of solutions of steady Stokes system with mixed boundary condition for sufficiently smooth data.

math.AP↗