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 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 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.

In this paper, we investigate CNF encodings, for which unit propagation is strong enough to derive a contradiction if the encoding is not consistent with a partial assignment of the variables (unit refutation complete or URC encoding) or additionally to derive all implied literals if the encoding is consistent with the partial assignment (propagation complete or PC encoding). We prove an exponential separation between the sizes of PC and URC encodings without auxiliary variables and strengthen the known results on their relationship to the PC and URC encodings that can use auxiliary variables. Besides of this, we prove that the sizes of any two irredundant PC formulas representing 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.

A matched formula is a CNF formula whose incidence graph admits a matching which matches a distinct variable to every clause. Such a formula is always satisfiable. Matched formulas are used, for example, in the area of parameterized complexity. We prove that the problem of counting the number of the models (satisfying assignments) of a matched formula is #P-complete. On the other hand, we define a class of formulas generalizing the matched formulas and prove that for a formula in this class one can choose in polynomial time a variable suitable for splitting the tree for the search of the models of the formula. As a consequence, the models of a formula from this class, in particular of any matched formula, can be generated sequentially with a delay polynomial in the size of the input. On the other hand, we prove that this task cannot be performed efficiently for linearly satisfiable formulas, which is a generalization of matched formulas containing the class considered above.

A matched formula is a CNF formula whose incidence graph admits a matching which matches a distinct variable to every clause. Such a formula is always satisfiable. Matched formulas are used, for example, in the area of parametrized complexity. We prove that the problem of counting the number of the models (satisfying assignments) of a matched formula is #P-complete. On the other hand, we define a class of formulas generalizing the matched formulas and prove that for a formula in this class one can choose in polynomial time a variable suitable for splitting the tree for the search of the models of the formula. As a consequence, the models of a formula from this class, in particular of any matched formula, can be generated sequentially with a delay polynomial in the size of the input. On the other hand, we prove that this task cannot be performed efficiently for linearly satisfiable formulas, which is a generalization of matched formulas containing the class considered above.

FL ew -algebras form the algebraic semantics of the full Lambek calculus with exchange and weakening. We investigate two relations, called satisfiability and positive satisfiability , between FL ew -terms and FL ew -algebras. For each FL ew -algebra, the sets of its satisfiable and positively satisfiable terms can be viewed as fragments of its existential theory; we identify and investigate the complements as fragments of its universal theory. We offer characterizations of those algebras that (positively) satisfy just those terms that are satisfiable in the two-element Boolean algebra providing its semantics to classical propositional logic. In case of positive satisfiability, these algebras are just the nontrivial weakly contractive FL ew -algebras. In case of satisfiability, we give a characterization by means of another property of the algebra, the existence of a two-element congruence. Further, we argue that (positive) satisfiability problems in FL ew -algebras are computationally hard. Some previous results in the area of term satisfiability in MV-algebras or BL-algebras are thus brought to a common footing with known facts on satisfiability in Heyting algebras.

Product Logic Π is an axiomatic extension of Hájek's Basic Fuzzy Logic BL coping with the 1-tautologies when the strong conjunction & and implication → are interpreted by the product of reals in [0, 1] and its residuum respectively. In this paper we investigate expansions of Product Logic by adding into the language a countable set of truth-constants (one truth-constant r\#304; for each r in a countable Π-subalgebra 𝒞 of [0, 1]) and by adding the corresponding book-keeping axioms for the truthconstants. We first show that the corresponding logics Π(𝒞) are algebraizable, and hence complete with respect to the variety of Π(𝒞)-algebras. The main result of the paper is the canonical standard completeness of these logics, that is, theorems of Π(𝒞) are exactly the 1-tautologies of the algebra defined over the real unit interval where the truth-constants are interpreted as their own values. It is also shown that they do not enjoy the canonical strong standard completeness, but they enjoy it for finite theories when restricted to evaluated Π-formulas of the kind r\#304; → φ, where r\#304; is a truth-constant and φ a formula not containing truth-constants. Finally we consider the logics ΠΔ(𝒞), the expansion of Π(𝒞) with the well-known Baaz's projection connective Δ, and we show canonical finite strong standard completeness for them.

A Boolean formula in a conjunctive normal form is called a $(k,s)$ – formula if every clause contains exactly k variables and every variable occurs in at most s clauses. The $(k,s)$–${\text{SAT}}$ problem is the SATISFIABILITY problem restricted to $(k,s)$–formulas. It is proved that for every $k \geqslant 3$ there is an integer $f(k)$ such that $(k,s)$–${\text{SAT}}$ is trivial for $s \leqslant f(k)$ (because every $(k,s)$–formula is satisfiable) and is NP-complete for $s \geqslant f(k) + 1$. Moreover, $f(k)$ grows exponentially with k, namely, $\lfloor {{{2^k } / {ek}}} \rfloor \leqslant f(k) \leqslant 2^{k - 1} - 2^{k - 4} - 1$ for $k \geqslant 4$.