The non-monotone dualization (NMD) is one of the most essential tasks required for finding hypotheses in various ILP settings, like learning from entailment [1, 2] and learning from interpretations [3]. Its task is to generate an irredundant prime CNF formula ψ of the dual f d where f is a general Boolean function represented by CNF [4]. The DNF formula φ of f d is easily obtained by De Morgan's laws interchanging the connectives of the CNF formula. Hence, the main task of NMD is to translate the DNF φ to an equivalent CNF ψ. This translation is used to find an alternative representation of the input form. For instance, given a set of models, it is desirable to seek underlying structure behind the models.
Example 1. Suppose that a set of models M are given as follows:
By treating M as the DNF formula, we translate it into CNF with NMD:
In fact, H is regarded as a hypothesis in learning from interpretations [
Monotone dualization (MD) is one such class that deals with monotone
Boolean functions for which CNF formulas are negation-free [
This paper aims at clarifying whether or not NMD can be solved using these techniques of MD, and if it can be then how it is realized. In general, it is not straightforward to use them because of the following two problems in NMD: – NMD has to treat redundant clauses like resolvents and tautologies.
Example 2. Let a CNF formula φ be (x1 ∨ x2) ∧ (x2 ∨ x3). If we treat negated
variables as regular variables, we can apply MD to φ and obtain the CNF
formula ψ = (x1 ∨ x2) ∧ (x1 ∨ x3) ∧ (x2 ∨ x2) ∧ (x2 ∨ x3). However, ψ contains
the tautology x2 ∨ x2 and the resolvent x1 ∨ x3 of x1 ∨ x2 and x2 ∨ x3.
– Unlike MD, the output of NMD is not necessarily unique. It is known that
the output of MD uniquely corresponds to the set of all the prime implicates
of f d [
By removing all tautologies from ψt, we obtain an irredundant CNF formula, denoted by ψir. Note that ψir is (x1 ∨ x2) ∧ (x2 ∨ x3) in Example 3.
We next address the second problem using a good property of ψir: a subset of the prime implicates is irredundant (i.e., an output of NMD) if and only if it subsumes ψir but never subsumes ψir if any clause is removed from it. This particular relation is called minimal subsumption. We then show that every subset satisfying the minimal subsumption is generated by MD. In this way, we reduce an original NMD problem into two MD problems: the one for computing ψir, and the other for generating a subset corresponding to an output of NMD. Due to space limitations, full proofs are omitted. 2 2.1
A Boolean function is a mapping f : {0, 1}n → {0, 1}. We write g |= f if f and g satisfy g(v) ≤ f (v) for all v ∈ {0, 1}n. g is (logically) equivalent to f , denoted by g ≡ f , if g |= f and f |= g. A function f is monotone if v ≤ w implies f (v) ≤ f (w) for all v, w ∈ {0, 1}n; otherwise it is non-monotone. Boolean variables x1, x2, . . . , xn and their negations x1, x2, . . . , xn are called literals. The dual of a function f , denoted by f d, is defined as f (x) where f and x is the negation of f and x, respectively.
A clause (resp. term) is a disjunction (resp. conjunction) of literals which is often identified with the set of its literals. It is known that a clause is tautology if it contains complementary literals. A clause C is an implicate of a function f if f |= C. An implicate C is prime if there is no implicate C′ such that C′ ⊂ C.
A conjunctive normal form (CNF) (resp. disjunctive normal form (DNF)) formula is a conjunction of clauses (resp. disjunction of terms) which is often identified with the set of clauses in it. A CNF formula φ is irredundant if φ ̸≡ φ − {C} for every clause C in φ; otherwise it is redundant. φ is prime if every clause in φ is a prime implicate of φ; otherwise it is non-prime. Let φ1 and φ2 be two CNF formulas. φ1 subsumes φ2, denoted by φ1 ≽ φ2, if there is a clause C ∈ φ1 such that C ⊆ D for every clause D ∈ φ2. In turn, φ1 minimally subsumes φ2, denoted by φ1 ≽♮ φ2, if φ1 subsumes φ2 but φ1 − {C} does not subsume φ2 for every clause C ∈ φ1.
Let φ be a CNF formula. τ (φ) denotes the CNF formula obtained by removing all tautologies from φ. We say φ is tautology-free if φ = τ (φ). Now, we formally define the dualization problem as follows.
Output: An irredundant prime CNF formula ψ such that
ψ is logically equivalent to φd
We call it monotone dualization (MD) if φ is negation-free; otherwise it is called
non-monotone dualization (NMD). As well known [
Definition 2 ((Minimal) Hitting set). Let Π be a finite set and F be a subset family of Π. A finite set E is a hitting set of F if for every F ∈ F , E ∩ F ̸= ∅. A finite set E is a minimal hitting set (MHS) of F if E satisfies that 1. E is a hitting set of F ; 2. For every subset E′ ⊆ E, if E′ is a hitting set of F , then E′ = E. Note that any CNF formula φ can be identified with the family of clauses in φ. Now, we consider the CNF formula, denoted by M (φ), which is the conjunction of all the MHSs of the family φ. Then, the following holds.
Theorem 1. [
Our motivation is to clarify whether or not any NMD problem can be reduced
into some MD problems. While MD is done by the state-of-the-art algorithms
to compute MHSs [
Example 5. Let the input CNF formula φ be {{x1, x2, x3}, {x1, x2, x3}}. τ (M (φ)) consists of the non-tautological prime implicates as follows: τ (M (φ)) = {{x1, x2}, {x1, x3}, {x2, x3}, {x1, x3}, {x1, x2}, {x3, x2}}. Then, we may notice that there are at least two irredundant subsets of τ (M (φ)): ψ1 = {{x1, x2}, {x1, x3}, {x2, x3}}. ψ2 = {{x1, x3}, {x1, x2}, {x3, x2}}. Indeed, ψ1 is equivalent to ψ2, and thus both are equivalent to τ (M (φ)). To address the two problems, this paper focuses on the following CNF formula. Definition 3 (Bottom formula). Let φ be a tautology-free CNF formula and T aut(φ) be { x ∨ x | φ contains both x and x }. Then, the bottom formula wrt φ (in short, bottom formula) is defined as the CNF formula τ (M (φ ∪ T aut(φ))). 3
Theorem 2. Let φ be a tautology-free CNF formula. Then, the bottom formula wrt φ is irredundant.
Example 6. Recall φ2 in Example 4. Then, T aut(φ2) is {x2∨x2}, and the bottom formula wrt φ2 is {{x1, x2}, {x2, x3}}. Indeed, it is irredundant, since it does not contain the resolvent {x1, x3}, unlike Example 4.
While any bottom formula is irredundant, it is not necessarily prime. Example 7. Recall the CNF formula φ in Example 5. Since T aut(φ) is the set {{x1, x1}, {x2, x2}, {x3, x3}}, the bottom formula is as follows: {{x1, x2, x3}, {x3, x2, x1}, {x3, x2, x1}, {x2, x3, x1}, {x2, x3, x1}, {x2, x3, x1}}. We write C1, C2, . . . , C6 for the above clauses in turn (i.e., C4 is {x2, x3, x1}). We then notice that the bottom formula is non-prime, because it contains a non-prime implicate C1 whose subset {x1, x2} is an implicate of φd. As shown in Example 7, the bottom formula itself is not necessarily an output of NMD. However, every NMD output is logically described with this formula. Theorem 3. Let φ be a tautology-free CNF formula. ψ is an output of NMD for φ iff ψ ⊆ τ (M (φ)) and ψ minimally subsumes the bottom formula wrt φ. Example 8. Recall Example 5 and Example 7. Fig. 1 describes the subsumption lattice bounded by two irredundant prime outputs ψ1 and ψ2 as well as the bottom formula {C1, C2, . . . , C6}. The solid (resp. dotted) lines show the subsumption relation between ψ1 (resp. ψ2) and the bottom formula. We then notice that both outputs ψ1 and ψ2 minimally subsume the bottom formula.
ψ1 {x1, x2} {x1, x3} {x2, x3} {x1, x3} {x1, x2} {x3, x2}
C1
C2
C3 C4 Bottom formula
C6 ψ2 C5 Theorem 3 shows that every NMD output ψ can be generated by selecting a subset ψ of τ (M (φ)) that minimally subsumes the bottom formula. Now, we show that the task of this selection is done by MD computation.
Let the bottom formula be {C1, C2, . . . , Cn}. We then denote by Si (1 ≤ i ≤ n) the set of clauses in τ (M (φ)) each of which is a subset of Ci. Fφ denotes the family of those sets {S1, S2, . . . , Sn}.
Theorem 4. Let φ be a tautology-free CNF formula. ψ is an output of NMD for φ if and only if ψ is an MHS of Fφ.
Example 9. Recall Example 8. We denote each clause of ψ1 and ψ2 in Fig. 4 by D1, . . . , D6, starting from left to right (i.e., D4 is {x1, x3}). Fφ is as follows: Fφ = {{D1, D4}, {D1, D6}, {D2, D6}, {D3, D4}, {D3, D5}, {D2, D5}}. By MHS computation, we have the five solutions, which contain {D1, D2, D3} and {D4, D5, D6} that correspond to ψ1 and ψ2, respectively. 5
This paper has presented a reduction technique from arbitrary NMD problem to two equivalent MD problems. Whereas algorithms and computation on MD has been extensively studied, it was not clarified whether or not NMD can be solved using the state-of-the-art MD computation. For this open problem, we give a solution how it is to be realized.
Our result can be used to investigate the complexity of NMD from the
viewpoint of MD computation. For instance, the complexity of generating one NMD
output can be described as follows:
(n + t + x)O(log(n+t+x)) + (x + 1)O(log(x+1)),
(1)
where n, t and x are the sizes of the input formula φ, the tautologies T aut(φ)
and the bottom formula τ (M (φ ∪ T aut(φ))), respectively. This is simply derived
from the result on the complexity of MD computation [