Resolution Simulates Ordered Binary Decision Diagrams for Formulas in Conjunctive Normal Form

TL;DR

This paper demonstrates that resolution can polynomially simulate Ordered Binary Decision Diagrams (OBDDs) when both are limited to formulas in Conjunctive Normal Form, resolving an open question about their relative efficiency.

Contribution

It proves that resolution and OBDDs are polynomially comparable on CNF formulas, challenging previous beliefs about their exponential separation.

Findings

Resolution simulates OBDDs polynomially on CNFs

Negates the existence of polynomial OBDD refutations with exponential resolution

Provides insights into the relative efficiency of proof systems in propositional logic

Abstract

A classical question of propositional logic is one of the shortest proof of a tautology. A related fundamental problem is to determine the relative efficiency of standard proof systems, where the relative complexity is measured using the notion of polynomial simulation. Presently, the state-of-the-art satisfiability algorithms are based on resolution in combination with search. An Ordered Binary Decision Diagram (OBDD) is a data structure that is used to represent Boolean functions. Groote and Zantema have proved that there is exponential separation between resolution and a proof system based on limited OBDD derivations. However, formal comparison of these methods is not straightforward because OBDDs work on arbitrary formulas, whereas resolution can only be applied to formulas in Conjunctive Normal Form (CNFs). Contrary to popular belief, we argue that resolution simulates OBDDs polynomially if we limit both to CNFs and thus answer negatively the open question of Groote and Zantema whether there exist unsatisfiable CNFs having polynomial OBDD refutations and requiring exponentially long resolution refutations.

Equations

$$\mathsf{F}:\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(\mathsf{B})\to \mathsf{Cls}(\phi )$$

$$\mathsf{Cls}(p,\phi )=\{C\in \mathsf{Cls}(\phi )\mid \exists \alpha \in \mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(p):C=\mathsf{F}(\alpha )\}$$

$$\gamma (p,C)=|\{\alpha \in \mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(p)\mid \mathsf{F}(\alpha )=C\}|-1$$

$$\tau (p,\phi )=\sum _{C\in \mathsf{Cls}(p,\phi )}\gamma (p,C)$$

$$\mathsf{Res}(p,\phi )=\{\psi \in \mathsf{Cnf}\mid \phi {⊢}_{\mathsf{res}}\psi \text{mbox}and\phi \wedge \psi ⊴{\mathsf{B}}^{\prime }\}$$

$$q^h{\sim }_p{q}^l$$

$$q{\to }_p{q}^{\prime }$$

$${\alpha }_1.x.{\alpha }_2/\models C$$

$${\alpha }_1.\neg x.{\alpha }_2/\models D$$

$$\phi =(x\vee \neg y)\wedge (y\vee z)\wedge (y\vee \neg z)\wedge \neg x$$

$$C_1=x\vee \neg y,C_2=y\vee z,C_3=y\vee \neg z,C_4=\neg x,$$

$$C_5=\mathsf{res}(C_2,C_3)=y,C_6=\mathsf{res}(C_1,C_5)=x,C_7=\mathsf{res}(C_4,C_6)=\perp$$

$$|\mathsf{Cls}(\psi )|\le |{\mathsf{Path}}^f(p)|/2$$

$$\neg (\exists C\in \mathsf{Cls}(\phi ):\alpha .\beta /\models C)⟹\mathsf{res}(\mathsf{F}(\alpha .x.\beta ),\mathsf{F}(\alpha .\neg x.\beta ))\in \mathsf{Cls}(\psi )$$

$$C_1=\neg x\vee \neg y\vee \neg v$$

$$D_1=x\vee \neg z\vee \neg v$$

$$\mathsf{res}(C_1,D_1)=\neg y\vee \neg z\vee \neg v$$

$$\mathsf{res}(C_4,D_2)=\neg y\vee z\vee \neg w$$

$$\mathsf{res}(C_3,D_3)=y\vee \neg z\vee \neg w$$

$$\alpha .x.\beta ,{\alpha }^{\prime }.x.{\beta }^{\prime }/\models C$$

$$\alpha .\neg x.\beta ,{\alpha }^{\prime }.\neg x.{\beta }^{\prime }/\models D$$

$$|\mathsf{Cls}(\psi )|\le |\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(p)|/2-k$$

$${\mathsf{PHP}}_n=\underset{i=1}{\overset{n+1}{\bigwedge }}\underset{j=1}{\overset{n}{\bigvee }}{p}_{ij}\wedge \underset{\begin{array}{c}1\le i<j\le n+1\\ 1\le k\le n\end{array}}{\bigwedge }\neg p_{ik}\vee \neg p_{jk}$$

$$p_0\vee C,\neg p_0\vee C\in \mathsf{Cls}({\overline{\mathsf{PHP}}}_n)$$

$$|\mathsf{Cls}(\psi )|\le |\mathsf{Cls}(\phi )|$$

$$|\mathsf{Cls}(\phi )|<|\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(p)|/2$$

$$P=\{(\alpha .x.\beta ,\alpha .\neg x.\beta )\mid \exists \alpha ,\beta :\alpha .x.\beta \in \mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(\mathsf{high}(p)),\alpha .\neg x.\beta \in \mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(\mathsf{low}(p))\}$$

$$({\alpha }_1.x.{\beta }_1,{\alpha }_1.\neg x.{\beta }_1),\dots ,({\alpha }_m.x.{\beta }_m,{\alpha }_m.\neg x.{\beta }_m)$$

$$|\mathsf{Cls}(\psi )|\le |\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(p)|-\tau (p,\phi )$$

$$|\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(q^{\prime })|-\tau (q^{\prime },\phi \wedge {\phi }^{\prime })\le |\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(q)|-\tau (q,\phi )$$

$$|\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(q^{\prime })|-\tau (q^{\prime },\phi \wedge {\phi }^{\prime })=|\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(q^{\prime })|-\tau (q^{\prime },\phi )=|\mathsf{Pat}{\mathsf{h}}^{\mathsf{f}}(q)|-\tau (q,\phi )$$

$$\alpha .\beta /\models \mathsf{res}(C,D)$$

Full text

Presently, the state-of-the-art satisfiability algorithms are based on resolution in combination with search. An Ordered Binary Decision Diagram (OBDD) is a data structure that is used to represent Boolean functions.

Groote and Zantema have proved that there is exponential separation between resolution and a proof system based on limited OBDD derivations. However, formal comparison of these methods is not straightforward because OBDDs work on arbitrary formulas, whereas resolution can only be applied to formulas in Conjunctive Normal Form (CNFs).

Contrary to popular belief, we argue that resolution simulates OBDDs polynomially if we limit both to CNFs and thus answer negatively the open question of Groote and Zantema whether there exist unsatisfiable CNFs having polynomial OBDD refutations and requiring exponentially long resolution refutations.

1 Introduction

Propositional proof complexity is the study of the lengths of proofs of statements expressed as propositional formulas. It is tightly connected in many ways to computational complexity, classical proof theory and practical questions of automated deduction.

A classical question of propositional proof complexity is one of the shortest proof of a tautology. A related fundamental problem is to determine the relative efficiency of standard proof systems, where the relative complexity is measured using the notion of polynomial simulation.

Proof systems. Propositional proof systems were defined by Cook and Reckhow as polynomial-time functions which have as their range the set of all tautologies [6]. They also noticed that if there is no propositional proof system that admits proofs polynomial in size of the input formula then the complexity classes NP and co-NP are different, and hence P$\neq$ NP.

In [2], Atserias, Kolaitis and Vardi generalised the notion of a refutational propositional proof system, viewing it as a special case of constraint propagation. Their proof system consists of the following four rules: (1) $\mathsf{Axiom}$ defines the initial set of constraints; (2) $\mathsf{Join}$ combines s two constraints by intersecting two relations and extending them to all variables occurring in either one of them; (3) $\mathsf{Projection}$ computes the projection of a constraint which is the existential quantification; (4) $\mathsf{Weakening}$ relaxes the constraint by enlarging its relation.

This generalisation brings the methods of constraint propagation to the area of proof complexity. On the other hand it introduces new classes of proof systems. The existing refutational proof systems can be viewed as a special case of this constraint propagation system.

Efficiency of proof systems. One of the most fundamental problems in the area of propositional proof complexity is to determine the relative efficiency of standard proof systems as it has been introduced by Cook and Reckhow in [6] who found it useful to separate the idea of providing a proof from that being efficient.

Proof systems are compared according to their strength using the notion of polynomial simulation. A proof system $S_{1}$ simulates polynomially a proof system $S_{2}$ if every tautology has proofs in $S_{1}$ of size at most polynomially larger than in $S_{2}$. Proof systems $S_{1}$ and $S_{2}$ are equivalent if they simulate each other polynomially.

Although substantial progress has been made in determining the relative complexity of proof systems and in proving strong lower bounds for some relatively weak proof systems, some major problems still remain unsolved.

As it is defined by Razborov in [14], the question of existence of an efficient proof has to be separated from another important question how to find such a proof efficiently and whether this search adds substantially to the inherent complexity of finding the shortest proof in a specific proof system. It is formalised by the notion of automatizability: a proof system is automatizabile if it produces a proof of a tautology in time polynomial in the size of its smallest proof [3].

The current proof systems of practical use are not automatizabile (or just weakly automatizabile). That is why in addition to lower bounds, there is practical interest in understanding relative efficiency of somewhat weaker proof systems. Interesting examples of such systems are those based either on general resolution or on classical OBDDs not utilising existential quantification.

Resolution versus OBDDs. In the automated reasoning community resolution and OBDDs are popular techniques for solving the propositional satisfiability problem abbreviated as SAT. In fact, both resolution and OBDDs are families of algorithms, where each corresponds to a specific way of making choices.

Resolution underlies the vast majority of all proof search techniques in this area. For example, the DPLL algorithm [7], as well as the clause learning methods are highly optimised implementations of resolution [12]. It has been shown in [13] that modern SAT solvers simulate resolution polynomially.

An OBDD is a canonical data structure that is used for the symbolic representation of Boolean functions [5, 19]. Atserias et al. introduced and studied a proof system operating with OBDDs as a special case of constraint propagation [2]. They proved that OBDD based refutations polynomially simulate resolution if they utilise existential quantification. That is OBDD based proof systems containing all four rules $\mathsf{Axiom}$, $\mathsf{Join}$, $\mathsf{Weakening}$ and $\mathsf{Projection}$ are strictly stronger than resolution but they are still exponential [9].

In the following we consider the OBDD proof system which contains just two rules, $\mathsf{Axiom}$ and $\mathsf{Join}$. These rules are equivalent to the $\mathsf{Apply}$ operator as it is defined in [5].

Benchmark studies show incomparable behaviour of resolution and such OBDD based systems [18]. Groote and Zantema proved that resolution and OBDDs do not simulate each other polynomially on arbitrary inputs for limited OBDD derivations [8]. Tveretina, Sinz and Zantema strengthened the above result and presented a class of CNFs hard for an arbitrary OBDD derivation and easy for resolution [17].

In general, formal comparison of resolution and OBDDs is not straightforward because the later work on arbitrary formulas, whereas resolution can take as an input only CNFs. We argue that resolution simulates OBDDs polynomially if we limit both to CNFs. Thus we answer negatively the open question of Groote and Zantema posed in [8] whether there exist unsatisfiable CNFs having polynomial OBDD refutations and requiring exponentially long resolution refutations.

Previous work. There are several works which study the relative efficiency of resolution based and OBDD based proof systems. The most relevant studies to our setting are the following ones.

Peltier shows in [11] that resolution augmented with the extension rule polynomially simulates OBDDs in the following sense: for any unsatisfiable formula $\varphi$ there exists a refutation of $\varphi$ with the size polynomially bounded by the maximal size of the reduced OBDDs corresponding to the subformulas occurring in $\varphi$. As mentioned before, Atserias et al prove in [2] that OBDD based refutations utilising existential quantification polynomially simulate resolution; moreover they are exponentially stronger. Groote and Zantema construct in [8] biconditinal formulas that have short OBDD refutations and after transforming them into CNFs they require exponentially long resolution proofs. But the same formulas after transformation into CNFs have exponentially long OBDD proofs.

Main result. We show that for any unsatisfiable CNF$\varphi$ there exists a resolution refutation of $\varphi$ with the size polynomially bounded by the size of an OBDD based refutation of $\varphi$ if it consists of two rules $\mathsf{Axiom}$ and $\mathsf{Join}$ and uses two standard reduction rules, elimination and merging. We now formally state the theorem.

Theorem 1.1

Assume an unsatisfiable CNF $\varphi$. If there is an OBDD refutation of $\varphi$ with two rules $\mathsf{Axiom}$ and $\mathsf{Join}$ of size $n$ then there is a resolution refutation of $\varphi$ of size $O(n^{2})$.

Our main argument is based on the idea that the elimination rule can be simulated by applying the resolution rule on the variable corresponding to the eliminated node [11]. But we use it differently.

We strengthen this idea and prove that the number of resolution steps corresponding to the elimination of a node is bounded by the number of clauses in the input CNF $\varphi$. Moreover, we show that it is an invariant property: although resolution steps generate new clauses, the number of resolution steps needed to simulate elimination of a node in an intermediate OBDD remains bounded by the number of clauses of $\varphi$ encoded by this OBDD. Furthermore, we show that it is sufficient to simulate only the elimination rule, that is the merging rule plays no role in the context.

The remainder of the paper. We give the necessary background in Section 2. In Section 3 we introduce two proof systems of interest: one is based on resolution and the other corresponds to OBDD derivations based on the Axion and Join rules. In Section 4 we show how to simulate the elimination rule using resolution and in Section 5 we prove our main result. Section 6 contains concluding remarks.

2 Preliminaries

2.1 Propositional Logic and Conjunctive Normal Forms

In this section we recall some basic notations about propositional logic and only provide a short overview of the main definitions.

In the following we consider propositional formulas in Conjunctive Normal Form (CNF) built using variables from a set $\mathsf{var}$. A literal $l$ is either a variable $x$ or its negation $\lnot x$ with $\mathsf{var}(l)=x$. A clause $C$ is a disjunction of literals, and a CNF $\varphi$ is a conjunction of clauses. By $\mathsf{Cnf}$ we denote the set of all CNFs.

We define $\mathsf{Cls}(\varphi)$ to be the set of clauses, $\mathsf{Lit}(\varphi)$ the set of literals, and $\mathsf{var}(\varphi)$ the set of variables contained in the CNF $\varphi$.

We use $\varphi|_{l}$ to denote the CNF obtained from $\varphi$ by deleting all clauses containing a literal $l$ and removing $\lnot l$ from the rest of the clauses. Note that $\varphi=\varphi|_{l}$ if $l\not\in\mathsf{Lit}(\varphi)$.

A truth assignment is a function $\mathsf{A}:\mathsf{var}\rightarrow\{\mathsf{true},\mathsf{false}\}$. We denote by $\mathcal{A}$ the set of all possible assignments. The truth values of literals, clauses and CNFs are defined in a standard way.

We write $\mathsf{A}\models\varphi$ if $\varphi$ evaluates to $\mathsf{true}$ for the assignment $\mathsf{A}$, otherwise we write $\mathsf{A}\not\models\varphi$. We say that $\varphi$ is unsatisfiable if $\mathsf{A}\not\models\varphi$ for any $\mathsf{A}\in\mathcal{A}$, otherwise it is satisfiable; $\varphi$ is a tautology if $\mathsf{A}\models\varphi$ for any $\mathsf{A}\in\mathcal{A}$.

We say that two CNFs $\varphi$ and $\psi$ are logically equivalent, denoted $\varphi\equiv\psi$, if $\mathsf{A}\models\varphi$ if and only if $\mathsf{A}\models\psi$ for any $\mathsf{A}\in\mathcal{A}$.

We use $\top$ for the empty set of clauses and $\bot$ for the CNF consisting of the empty clause. By definition the empty clause is unsatisfiable that is it is equivalent to $\mathsf{false}$, and the the empty set of clauses is equivalent to $\mathsf{true}$.

2.2 Ordered Binary Decision Diagrams

The concept of ordered binary decision diagrams (OBDDs) was first proposed by Lee in [10] as a means to represent propositional formulas (Boolean functions) compactly as directed acyclic graphs (DAGs). Then it was further developed to a data structure by Acers [1] and Boute [4], and subsequently by Bryant [5].

Definition 1 (An OBDD)

An OBDD $\mathsf{B}$ is a directed acyclic graph satisfying the following:

it has a unique node called the root and denoted by $\mathsf{root}(\mathsf{B})$; 2. 2.

each inner node $p$ is labeled by the propositional variable $\mathsf{var}(p)$ and has exactly two successors, a $\mathsf{false}$-successor and a $\mathsf{true}$-successor; 3. 3.

the inner nodes build the set $\mathsf{Node}(\mathsf{B})$, and the labels build the set $\mathsf{var}(\mathsf{B})$; 4. 4.

each leaf node is labeled by either $\mathsf{true}$ or $\mathsf{false}$; 5. 5.

there is a total variable order $\prec$ such that for each transition from the inner node with label $x$ to the inner node with label $y$ we have that $x\prec y$.

We use $\mathsf{high}(p)$ and $\mathsf{low}(p)$ to denote the OBDDs rooted at the $\mathsf{true}$-successor and the $\mathsf{false}$-successor of $p$; $|\mathsf{B}|$ is the size of $\mathsf{B}$, that is the number of its inner nodes.

We use $\mathsf{B}_{1}\equiv\mathsf{B}_{2}$ to denote that $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ are isomorphic OBDDs defined as follows:

• •

both $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ consist either of the node $\mathsf{true}$ or of the node $\mathsf{false}$;

• •

$\mathsf{var}(\mathsf{root}(\mathsf{B}_{1}))=\mathsf{var}(\mathsf{root}(\mathsf{B}_{2}))$, $\mathsf{high}(\mathsf{B}_{1})\equiv\mathsf{high}(\mathsf{B}_{2})$ and $\mathsf{low}(\mathsf{B}_{1})\equiv\mathsf{low}(\mathsf{B}_{2})$.

OBDD operations are applicable only to OBDDs that respect the same variable ordering. To shorten the notations in the rest of the paper, we assume without explicitly stating that all the variables agree on the common variable order $x_{1}\prec x_{2}\prec x_{3}\prec\dots$ when considering different OBDDs in the same context.

Definition 2 (Path)

A path of an OBDD $\mathsf{B}$ is a sequence $\alpha=l_{1}\ldots l_{k}$ of literals with $k\geq 1$ such that there are $p_{1},\ldots,p_{k}\in\mathsf{Node}(\mathsf{B})$, where

• •

$p_{1}=\mathsf{root}(\mathsf{B})$;

• •

for $1\leq i<k$, either $p_{i+1}=\mathsf{root}(\mathsf{high}(p_{i}))$ and $l_{i}=\mathsf{var}(p_{i})$, or $p_{i+1}=\mathsf{root}(\mathsf{low}(p_{i}))$ and $l_{i}=\neg\mathsf{var}(p_{i})$;

• •

$\mathsf{high}(p_{k})\in\{\mathsf{false},\mathsf{true}\}$ if $l_{k}=\mathsf{var}(p_{k})$;

• •

$\mathsf{low}(p_{k})\in\{\mathsf{false},\mathsf{true}\}$ if $l_{k}=\lnot\mathsf{var}(p_{k})$.

We use $\mathsf{Path}(\mathsf{B})$ to denote the set of all paths of $\mathsf{B}$, and $\mathsf{Path^{f}}(\mathsf{B})$ to denote the set of all paths that go to the $\mathsf{false}$ node. By $\mathsf{Path}(p)$ we mean the set of all paths that go through the inner node $p$, and $\mathsf{Path^{f}}(p)=\mathsf{Path}(p)\cap\mathsf{Path^{f}}(\mathsf{B})$.

A path can be seen as a conjunction of literals. In this way, each path $\alpha=l_{1}\ldots l_{k}$ naturally induces the set $\mathcal{A}(\alpha)$ of truth assignments evaluating each $l_{i}$ to $\mathsf{true}$. We write $\alpha\not\models C$ for a clause $C$ if $A\not\models C$ for any $A\in\mathcal{A}(\alpha)$. Where it is convenient, we see a path as a set of literals and use the set notations.

We say that a CNF $\varphi$ and an OBDD $\mathsf{B}$ are logically equivalent if for every assignment $\mathsf{A}\in\mathcal{A}$, $\alpha\not\models\varphi$ if and only if there is a path $\alpha\in\mathsf{Path^{f}}(\mathsf{B})$ such that $\mathsf{A}\in\mathcal{A}(\alpha)$.

For any CNF $\varphi$ and OBDD $\mathsf{B}$, we use $\varphi\unlhd\mathsf{B}$ to denote that $\varphi$ and $\mathsf{B}$ are logically equivalent and for each path $\alpha\in\mathsf{Path^{f}}(\mathsf{B})$ there is a clause $C\in\mathsf{Cls}(\varphi)$ such that $\alpha\not\models C$.

2.3 OBDD Construction

The straightforward way to construct an OBDD is to start with a binary decision tree and then incrementally eliminate redundancies and identify identical subtrees. The other more efficient way follows the structure of the propositional formula. Such algorithms start with building OBDDs for variables or literals, and then construct more complex OBDDs by using OBDD operations for logical connectives.

Algorithm 1 presented below (from [16]) takes as an input two OBDDs $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ and returns their conjunction denoted by $\mathsf{B}_{1}\land\mathsf{B}_{2}$. It proceeds from the root downward creating vertices in the resulting graph as follows:

the function ${\small{\mathsf{Dec}}}$ decomposes a non-terminal OBDD node into its constituent components, that is its variable and cofactors; 2. 2.

the function ${\small{\mathsf{Node}}}$ constructs a new OBDD node if it is not already present, and otherwise returns the already existent node.

Lemma 1 is a technical lemma which will be used to prove Corollary 1. It follows relatively straightforwardly from the definition of Algorithm 1.

Lemma 1

Assume OBDDs $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ such that $\mathsf{var}(\mathsf{B}_{1})\neq\emptyset$ and $\mathsf{var}(\mathsf{B}_{2})\neq\emptyset$. Then Algorithm 1 returns the OBDD $\mathsf{B}_{1}\land\mathsf{B}_{2}$ such that

• •

for each $\alpha\in\mathsf{Path^{f}}(\mathsf{B}_{1}\land\mathsf{B}_{2})$ there is $\beta\in\mathsf{Path^{f}}(B_{1})\cup\mathsf{Path^{f}}(B_{2})$ such that $\beta\subseteq\alpha$;

• •

for each $\beta\in\mathsf{Path^{f}}(B_{1})\cup\mathsf{Path^{f}}(B_{2})$ there is $\alpha\in\mathsf{Path^{f}}(\mathsf{B}_{1}\land\mathsf{B}_{2})$ such that $\beta\subseteq\alpha$.

Proof

We give a proof by induction on $k=|\mathsf{var}(\mathsf{B}_{1})\cup\mathsf{var}(\mathsf{B}_{2})|$. For the basis step we choose $k=0$ and the lemma trivially holds.

We assume that the lemma holds for any $\mathsf{B}_{1}^{\prime}$ and $\mathsf{B}_{2}^{\prime}$ such that $|\mathsf{var}(\mathsf{B}^{\prime}_{1})\cup\mathsf{var}(\mathsf{B}^{\prime}_{2})|\leq k-1$. Let $|\mathsf{var}(\mathsf{B}_{1})\cup\mathsf{var}(\mathsf{B}_{2})|=k$ and $x\in\mathsf{var}(\mathsf{B}_{1})\cup\mathsf{var}(\mathsf{B}_{2})$ be the smallest variable. Then by the definition of an OBDD $|\mathsf{var}(\mathsf{high}(\mathsf{B}_{1}\wedge\mathsf{B}_{2}))|\leq k-1$ and $|\mathsf{var}(\mathsf{low}(\mathsf{B}_{1}\wedge\mathsf{B}_{2}))|\leq k-1$.

If $x\in\mathsf{var}(\mathsf{B}_{1})$ and $x\in\mathsf{var}(\mathsf{B}_{2})$ then by the definition of Algorithm 1 it returns the OBDD $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ such that

• •

$\mathsf{var}(\mathsf{root})=x$;

• •

$\mathsf{high}(\mathsf{B}_{1}\wedge\mathsf{B}_{2})=\mathsf{high}(\mathsf{B}_{1})\wedge\mathsf{high}(\mathsf{B}_{2})$ and $\mathsf{low}(\mathsf{B}_{1}\wedge\mathsf{B}_{2})=\mathsf{low}(\mathsf{B}_{1})\wedge\mathsf{low}(\mathsf{B}_{2})$.

If $x\in\mathsf{var}(\mathsf{B}_{1})$ and $x\not\in\mathsf{var}(\mathsf{B}_{2})$ then by the definition of Algorithm 1 it returns the OBDD $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ such that

• •

$\mathsf{var}(\mathsf{root})=x$;

• •

$\mathsf{high}(\mathsf{B}_{1}\wedge\mathsf{B}_{2})=\mathsf{high}(\mathsf{B}_{1})\wedge\mathsf{B}_{2}$ and $\mathsf{low}(\mathsf{B}_{1}\wedge\mathsf{B}_{2})=\mathsf{low}(\mathsf{B}_{1})\wedge\mathsf{B}_{2}$.

We use the induction hypothesis and conclude that the lemma holds.

The following corollary is a direct consequence of Lemma 1 and it will be used later to prove the main result.

Corollary 1

Assume CNFs $\varphi_{1}$ and $\varphi_{2}$ and OBDDs $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ such that $\varphi_{1}\unlhd\mathsf{B}_{1}$ and $\varphi_{2}\unlhd\mathsf{B}_{2}$. Then Algorithm 1 returns the OBDD $\mathsf{B}_{1}\land\mathsf{B}_{2}$ such that $\varphi_{1}\land\varphi_{2}\unlhd\mathsf{B}_{1}\land\mathsf{B}_{2}$.

2.4 Reduction Rules

There are two reduction rules not affecting the semantics of OBDDs that can be used to reduce the size of the OBDDs constructed by Algorithm 1 defined as follows.

• •

Merging: If $\mathsf{low}(p)\equiv\mathsf{low}(q)$ and $\mathsf{high}(p)\equiv\mathsf{high}(q)$ for $p,q\in\mathsf{Node}(\mathsf{B})$ then the node $p$ can be removed. Any link to the node $p$ is replaced by a link to the node $q$.

• •

Elimination: If $\mathsf{low}(p)\equiv\mathsf{high}(p)$ for $p\in\mathsf{Node}(\mathsf{B})$ then the node $p$ can be removed. Any link to the node $p$ is replaced by a link to the root of $\mathsf{high}(p)$. We write $\mathsf{B}\rightarrow_{p}\mathsf{B}^{\prime}$ if $\mathsf{B}^{\prime}$ is obtained from $\mathsf{B}$ by eliminating the node $p$.

We use $\mathsf{B}^{\downarrow}$ to denote the reduced OBDD obtained from $\mathsf{B}$, that is no reduction rule can be applied to $\mathsf{B}^{\downarrow}$ any more.

Lemma 2 (Bryant [5])

If $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ are logically equivalent OBDDs then $\mathsf{B}_{1}^{\downarrow}\equiv\mathsf{B}_{2}^{\downarrow}$.

The total time complexity of the algorithm is $O(|\mathsf{B}_{1}|\times|\mathsf{B}_{2}|)$. In the worst case, the upper bound is achieved and $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ can contain $O(|\mathsf{B}_{1}|\times|\mathsf{B}_{2}|)$ nodes.

Theorem 2.1 (Bryant [5])

Let $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ be two reduced OBDDs, that is $\mathsf{B}_{1}\equiv\mathsf{B}_{1}^{\downarrow}$ and $\mathsf{B}_{2}\equiv\mathsf{B}_{2}^{\downarrow}$. Then the size of $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ is $O(|\mathsf{B}_{1}|\times|\mathsf{B}_{2}|)$, and the number of merging and elimination steps to compute the reduced OBDD corresponding to $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ is at most $|\mathsf{B}_{1}\wedge\mathsf{B}_{2}|$.

Proof

By definition, any subOBDD of $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ is of the form $\mathsf{B}^{\prime}_{1}\wedge\mathsf{B}^{\prime}_{2}$, where $\mathsf{B}^{\prime}_{1}$ and $\mathsf{B}^{\prime}_{2}$ are subOBDDs of $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ respectively. Hence, the size of $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ is bounded by $O(|\mathsf{B}_{1}|\times|\mathsf{B}_{2}|)$. 2. 2.

This is immediate since the elimination and merging rules strictly decrease the number of nodes.

2.5 Notations and Technical Background

Now we define notations that will be used in the rest of the paper and introduce some simple technical background we need to prove the main result. Thus, some additional properties related to the construction of an OBDD by Algorithm 1 are introduced in Lemma 3 and straightforward combinatorial results are defined in Lemma 4.

Let $\varphi$ be a CNF and $\mathsf{B}$ be an OBDD such that $\varphi\unlhd\mathsf{B}$. We tacitly assume a function

[TABLE]

such that $\alpha\not\models\mathsf{F}(\alpha)$ for an $\alpha\in\mathsf{Path^{f}}(\mathsf{B})$. For each node $p\in\mathsf{Node}(\mathsf{B})$, we define the set

[TABLE]

For each $C\in\mathsf{Cls}(\varphi)$ and $p\in\mathsf{Node}(\mathsf{B})$, we define

[TABLE]

and

[TABLE]

Suppose $\mathsf{high}(p)\equiv\mathsf{low}(p)$ and $\mathsf{B}\rightarrow_{p}\mathsf{B}^{\prime}$ for a node $p\in\mathsf{Node}(\mathsf{B})$ and an OBDD $\mathsf{B}^{\prime}$. The set $\mathsf{Res}(p,\varphi)$ is defined as follows:

[TABLE]

Let $x=\mathsf{var}(p)$ and $q^{h}\in\mathsf{Node}(\mathsf{high}(p))$ and $q^{l}\in\mathsf{Node}(\mathsf{low}(p))$. We write

[TABLE]

to denote that $\alpha.x.\beta\in\mathsf{Path^{f}}(q^{h})$ if and only if $\alpha.\lnot x.\beta\in\mathsf{Path^{f}}(q^{l})$ for some $\alpha$ and $\beta$.

Let $\mathsf{B}\rightarrow_{p}\mathsf{B}^{\prime}$. For simplicity, we define informally what we mean by $q\rightarrow_{p}q^{\prime}$. The OBDD $\mathsf{B}^{\prime}$ contains in fact the same nodes as $\mathsf{B}$ except the node $p$. We write

[TABLE]

to denote that the node $q^{\prime}\in\mathsf{Node}(\mathsf{B}^{\prime})$ is in fact the node $q\in\mathsf{Node}(\mathsf{B})$ after renaming as $q^{\prime}$.

In the following we assume that clauses of $\varphi$ are not subsumed while constructing the OBDD encoding it using Algorithm 1. This is formalised with Lemma 3 below.

Lemma 3

Assume a CNF $\varphi$ and an OBDD $\mathsf{B}$ such that $\varphi\unlhd\mathsf{B}$. Let $\mathsf{high}(p)\equiv\mathsf{low}(p)$ for some $p\in\mathsf{Node}(\mathsf{B})$ with $x=\mathsf{var}(p)$. Suppose the following holds:

$C\in\mathsf{Cls}(\mathsf{high}(p),\varphi)$* and $D\in\mathsf{Cls}(\mathsf{low}(p),\varphi)$;* 2. 2.

Let $C=\lnot x\vee C^{\prime}$ and $D=x\vee D^{\prime}$. Then for any literal $l$, if $l\in\mathsf{Lit}(C^{\prime})$ then $\lnot l\not\in\mathsf{Lit}(D^{\prime})$; 3. 3.

There is $x^{\prime}\in\mathsf{var}(C)\cap\mathsf{var}(D)$ such that for any $x^{\prime\prime}\in var(C)\cup\mathsf{var}(D)\backslash\{x^{\prime}\}$, $x^{\prime\prime}\prec x^{\prime}$.

Then for some $\alpha_{1},\alpha_{2}$ there are $\alpha_{1}.x.\alpha_{2}\in\mathsf{Path^{f}}(\mathsf{high}(p))$ and $\alpha_{1}.\lnot x.\alpha_{2}\in\mathsf{Path^{f}}(\mathsf{low}(p))$ such that

[TABLE]

[TABLE]

Proof

In fact, the lemma statement is implied directly by the assumption $\mathsf{high}(p)\equiv\mathsf{low}(p)$ and the definition of Algorithm 1. But we will provide a somewhat formal proof by induction on $k=|\mathsf{var}(\mathsf{Path^{f}}(p))|$.

Let $k=1$. Now we obtain that $\alpha_{1}=\alpha_{2}=\varepsilon$ where $\varepsilon$ is the empty string and the lemma holds. We assume that the lemma holds for $k$ with $k\geq 1$ and show that it hold for $k+1$. We consider the following cases:

• •

The node $p$ is not the root of $\mathsf{B}$. Then the lemma holds by the induction hypothesis and the definition of Algorithm 1 for $\mathsf{high}(\mathsf{root}(\mathsf{B}))$ and $\varphi|_{\lnot\mathsf{var}(\mathsf{root}(\mathsf{B}))}$ or for $\mathsf{low}(\mathsf{root}(\mathsf{B}))$ and $\varphi|_{\mathsf{var}(\mathsf{root}(\mathsf{B}))}$. Now the lemma holds straightforwardly for $\mathsf{B}$ and $\varphi$.

• •

The node $p$ is the root of $\mathsf{B}$. Let $q^{h}=\mathsf{root}(\mathsf{high}(p))$ and $q^{l}=\mathsf{root}(\mathsf{low}(p))$. It follows from $\mathsf{high}(p)\equiv\mathsf{low}(p)$ that $\mathsf{high}(q^{h})\equiv\mathsf{high}(q^{l})$ and $\mathsf{low}(q^{h})\equiv\mathsf{low}(q^{l})$.

We construct the OBDD $\mathsf{B}^{h}$ by redirecting there true and false branches of $p$ to the $\mathsf{root}(\mathsf{high}(q^{h}))$ and $\mathsf{root}(\mathsf{high}(q^{l}))$ correspondingly; and $\mathsf{B}^{l}$ by redirecting there true and false branches of $p$ to the $\mathsf{root}(\mathsf{low}(q^{h}))$ and $\mathsf{root}(\mathsf{low}(q^{l}))$ correspondingly. Let $y=\mathsf{root}(q^{h})=\mathsf{root}(q^{l})$. By the induction hypothesis the lemma holds for $\mathsf{B}^{h}$ and $\varphi|_{\lnot y}$ or for $\mathsf{B}^{l}$ and $\varphi|_{y}$. Hence, the lemma holds for arbitrary $\mathsf{B}$ and $\varphi$.

Lemma below presents some technical results which will be used to prove Theorem 6.

Lemma 4

Let $S$ be a finite set such that $|S|>0$, and $B_{1},\dots,B_{l}\subseteq S$ be a sequence with:

• •

$B_{l}=S$**

• •

For each $B_{i}$, $1\leq i<l$, one of the following holds:

• –

$B_{i}=\{s\}$* for $s\in S$*

• –

$B_{i}=B_{j}\cup B_{k}$* for some $j,k$ with $j<k<i$*

Then $l=2|S|-1$.

Proof

We give a proof by induction on $|S|$. As the basis step we choose $|S|=1$. Then the lemma hold as trivially $l=1$. Let the lemma hold for any $|S|$. Assume a set $S^{\prime}$ such that $|S^{\prime}|=|S|+1$. Then $l^{\prime}=l+2=(2|S|-1)+2=2|S^{\prime}|-1$.

3 OBDDs and Resolution as Proof Systems

Proof systems based on resolution and OBDDs are so-called refutational proof systems. A refutation of an unsatisfiable CNF $\varphi$ starts with the clauses of $\varphi$ and derives a contradiction represented by the empty clause $\bot$ for resolution and by the $\mathsf{false}$ node for OBDDs.

Any proof system operating with OBDDs can be seen as an instance of the constraints based proof system. In the following we consider the OBDD proof system which uses two rules, $\mathsf{Axiom}$ and $\mathsf{Join}$.

Definition 3 (OBDD refutation)

An OBDD refutation of a CNF $\varphi$ is a sequence of OBDDs $\mathsf{B}_{1},\dots,\mathsf{B}_{k}$ such that the following holds:

• •

$\mathsf{Axiom}:$ $\mathsf{B}_{i}\equiv C_{i}$ with $1\leq i\leq|\mathsf{Cls}(\varphi)|$;

• •

$\mathsf{Join}:$ $\mathsf{B}_{i}\equiv\mathsf{B}^{\downarrow}_{j^{\prime}}\wedge\mathsf{B}^{\downarrow}_{j^{\prime\prime}}$ with $1\leq j^{\prime}<j^{\prime\prime}<i$ and $|\mathsf{Cls}(\varphi)|<i\leq k$;

• •

$\mathsf{B}^{\downarrow}_{k}\equiv\mathsf{false}$.

The size of the OBDD refutation is defined as $\sum_{i=1}^{k}|\mathsf{B}_{i}|$.

Without loss of generality we can assume that each OBDD is used exactly once, that is if a CNF $\varphi$ consists of $m$ clauses then the number of OBDDs in the OBDD refutation of $\varphi$ is exactly $2m-1$.

The resolution proof system goes back to Robinson [15] and consists of a single rule. It derives from two clauses $l\vee C$ and $\lnot l\vee D$, such that $C$ and $D$ do not contain a complementary literal, the new clause $C\vee D$ called the resolvent of $l\vee C$ and $\lnot l\vee D$, and denoted in the following by $\mathsf{res}(l\vee C,\lnot l\vee D)$.

When we write $\mathsf{res}(C,D)$, we assume that there is a literal $l$ such that $l\in\mathsf{Lit}(C)$ and $\lnot l\in\mathsf{Lit}(D)$; moreover, the clauses $C$ and $D$ contain no other complimentary literals.

Definition 4 (Resolution refutation)

A resolution refutation of a CNF $\varphi$ of size $k$ is a sequence of clauses $C_{1},\dots,C_{k}$ such that

$\mathsf{Axiom}:$ $C_{i}\in\mathsf{Cls}(\varphi)$ with $1\leq i\leq|\mathsf{Cls}(\varphi)|$; 2. 2.

$\mathsf{Join}:$ $C_{i}=\mathsf{res}(C_{j^{\prime}},C_{j^{\prime\prime}})$ with $1\leq j^{\prime}<j^{\prime\prime}<i$ and $|\mathsf{Cls}(\varphi)|<i\leq k$; 3. 3.

$C_{k}=\bot$.

We say that $k$ is the size of the resolution refutation. We write $\varphi\vdash_{\mathsf{res}}\psi$ for any CNF $\psi$ such that $\psi=\bigwedge_{i=|\mathsf{Cls}(\varphi)|+1}^{k^{\prime}}C_{i}$ with $k^{\prime}\leq k$.

4 Simulating OBDDs by Resolution

In the rest of the paper we show formally that if there is an OBDD refutation of a CNF $\varphi$ of size $n$ then there is a resolution refutation of $\varphi$ of size at most $n^{2}$. The existence of such resolution refutation is based on the following observations:

elimination of a node can be simulated by at most $|\mathsf{Cls}(\varphi)|$ resolution steps; 2. 2.

$|\mathsf{Cls}(\varphi)|\leq n$; 3. 3.

the number of nodes which can be removed by the elimination rule is at most $n$.

Our main argument is based on the idea that the elimination rule can be simulated by applying the resolution rule on the variable corresponding to the eliminated node [11].

We strengthen this idea and prove that the number of resolution steps corresponding to the elimination of a node is bounded by the number of clauses in the input CNF $\varphi$.

Moreover, we show that it is an invariant property: although resolution steps generate new clauses, the number of resolution steps needed to simulate elimination of a node in an intermediate OBDD remains bounded by the number of clauses of $\varphi$ encoded by this OBDD. We also show that it is sufficient to simulate only the elimination rule. As the merging rule plays no role in the context, we assume for simplicity that all intermediate OBDDs are merged.

Example 1

Before giving technical details, we provide a simple illustrating example. We consider the CNF

[TABLE]

An OBDD refutation of $\varphi$ is depicted in Figure 1. The OBDDs $\mathsf{B}_{6}^{\downarrow}$ and $\mathsf{B}_{7}^{\downarrow}$ are obtained from $\mathsf{B}_{6}$ and $\mathsf{B}_{7}$ correspondingly by applying the elimination rule.

Consider the following resolution refutation of $\varphi$:

[TABLE]

[TABLE]

It simulates the OBDD refutation as follows:

• •

By resolving the clauses $C_{2}$ and $C_{3}$ we eliminate the occurrences of $z$. By resolving the clauses $C_{1}$ and $C_{5}$ we eliminate the occurrences of $y$. The new set of clauses decodes the OBDD $\mathsf{B}_{6}^{\downarrow}$.

• •

By resolving the clauses $C_{4}$ and $C_{6}$ we eliminate the occurrences of $x$ in $\mathsf{B}_{7}$.

4.1 Simulation of the Elimination Rule

In this section we show that elimination of a node can be simulated by at most $|\mathsf{Cls}(\varphi)|$ resolution steps, where $\varphi$ is the input unsatisfiable CNF.

Lemma 5 demonstrates that elimination of a node $p$ can be simulated by at most $k/2$ resolution steps, where $k$ is the number of paths going through $p$ to the $\mathsf{false}$-node. This is a variant of Lemma 2 from [11] which serves our needs better.

Lemma 5

Assume a CNF $\varphi$ and an OBDD $\mathsf{B}$ such that $\varphi\unlhd\mathsf{B}$. Let $\mathsf{B}\rightarrow_{p}\mathsf{B}^{\prime}$ for a node $p\in\mathsf{Node}(\mathsf{B})$ and an OBDD $\mathsf{B}^{\prime}$. Then there is a CNF $\psi\in\mathsf{Res}(p,\varphi)$ such that

[TABLE]

Proof

Assume that $x=\mathsf{var}(p)$. Let $\psi$ be the smallest CNF satisfying the following: for all $\alpha$ and $\beta$ such that $\alpha.x.\beta,\alpha.\lnot x.\beta\in\mathsf{Path^{f}}(p)$,

[TABLE]

By construction, $\psi\in\mathsf{Res}(p,\varphi)$ and $|\mathsf{Cls}(\psi)|\leq|\mathsf{Path}^{f}(p)|/2$.

Example 2

We provide another illustrating example. Consider the CNF $\varphi$ consisting of the following eight clauses:

[TABLE]

Figure 2 represents the OBDD encoding of $\varphi$, and the mapping of the $\mathsf{false}$-paths onto the clauses of $\varphi$.

Elimination of the node labelled with $x$ can be simulated by the following resolution steps:

[TABLE]

Corollary 2 below follows directly from Theorem 5.

Corollary 2

Assume an OBDD $\mathsf{B}$ and a CNF $\varphi$ such that $\varphi\unlhd\mathsf{B}$. Suppose $\mathsf{high}(p)\equiv\mathsf{low}(p)$ for some $p\in\mathsf{Node}(\mathsf{B})$. Let $\mathsf{P}^{h}\subseteq\mathsf{Path^{f}}(\mathsf{high}(p))$ and $\mathsf{P}^{l}\subseteq\mathsf{Path^{f}}(\mathsf{low}(p))$ be sets such that $\alpha.x.\beta\in\mathsf{P}^{h}$ if and only if $\alpha.\lnot x.\beta\in\mathsf{P}^{l}$ for some $\alpha$ and $\beta$. Suppose $\mathsf{\overline{P}}^{h}=\mathsf{Path^{f}}(\mathsf{high}(p))\backslash\mathsf{P}^{h}$ and $\mathsf{\overline{P}}^{l}=\mathsf{Path^{f}}(\mathsf{low}(p))\backslash\mathsf{P}^{l}$. Suppose for each pair of paths $(\alpha.x.\beta,\alpha.\lnot x.\beta)\in\mathsf{\overline{P}}^{h}\times\mathsf{\overline{P}}^{l}$ there is a pair of paths $(\alpha^{\prime}.x.\beta^{\prime},\alpha^{\prime}.\lnot x.\beta^{\prime})\in\mathsf{P}^{h}\times\mathsf{P}^{l}$ and clauses $C,D\in\mathsf{Cls}(\varphi)$ such that

[TABLE]

[TABLE]

Let $k=|\mathsf{\overline{P}}^{h}|$. Then there is $\psi\in\mathsf{Res}(p,\varphi)$ such that

[TABLE]

Example 3

The formulas $\mathsf{PHP}_{n}$, $n\geq 1$, encoding the pigeonhole principle were studied intensively in relation to complexity of different propositional proof systems and they are defined as follows.

[TABLE]

We build the formulas $\mathsf{\overline{PHP}}_{n}$ by doubling the number of clauses of $\mathsf{PHP}_{n}$: for some new variable $p_{0}$

[TABLE]

if and only if $C\in\mathsf{Cls}(\mathsf{PHP}_{n})$.

Let $\mathsf{B}$ be the OBDD encoding $\mathsf{\overline{PHP}}_{2}$ as it is depicted in Figure 3. Elimination of the node $p_{0}$ can be trivially simulated by $|\mathsf{Cls}(\mathsf{PHP}_{2})|$ resolution steps. It is sufficient to add the resolvent $\mathsf{res}(p_{0}\vee C,\lnot p_{0}\vee C)=C$.

While the size of the OBDDs encoding $\mathsf{\overline{PHP}}_{n}$ will grow exponentially in $n$, elimination of the node labelled with $p_{0}$ can be simulated in the same manner by the number of resolution steps bounded by $|\mathsf{Cls}(\mathsf{\overline{PHP}}_{n})|$ which grows polynomially in $n$.

The subsequent statements improve the upper bound on the number of resolution steps needed to simulate elimination of an arbitrary node. Namely, we show that the number of resolution steps sufficient to simulate elimination of a node $p$ is bounded by $|\mathsf{Cls}(\varphi)|$.

Lemma 6

Let $\varphi$ be a CNF and $\mathsf{B}$ be an OBDD such that $\varphi\unlhd\mathsf{B}$. Suppose $\mathsf{B}\rightarrow_{p}\mathsf{B}^{\prime}$ for some $p\in\mathsf{Node}(\mathsf{B})$ and $\mathsf{B}^{\prime}$. Then there is a CNF $\psi\in\mathsf{Res}(p,\varphi)$ such that

[TABLE]

Proof

If $|\mathsf{Cls}(\varphi)|\geq|\mathsf{Path^{f}}(p)|/2$ then the theorem holds by Theorem 5. We assume that

[TABLE]

Let $m=|\mathsf{Path^{f}}(p)|/2$ and $m^{\prime}=|\mathsf{Cls}(\varphi)|$ with $m^{\prime}-m>0$; and $p^{h}=\mathsf{root}(\mathsf{high}(p))$, $p^{l}=\mathsf{root}(\mathsf{low}(p))$ and $x=\mathsf{var}(p)$. Let $P$ be the following set

[TABLE]

Assume a function $\mathsf{F}^{\prime}:P\rightarrow\mathsf{Cls}(\varphi)$ such that $\mathsf{F}^{\prime}((\alpha.x.\beta,\alpha.\lnot x.\beta))=C$ if $\alpha.x.\beta\not\models C$ or $\alpha.\lnot x.\beta\not\models C$ and $\bigcup_{(\alpha.x.\beta,\alpha.\lnot x.\beta)\in P}\mathsf{F}^{\prime}((\alpha.x.\beta,\alpha.\lnot x.\beta))=\mathsf{Cls}(p,\varphi)$.

We define the sets $S,S_{1},\dots,S_{l}$ with $l=2m-1$ as follows:

• •

$S=P$;

• •

$S_{i}=\{s_{i}\}$ for $s_{i}\in S^{\prime}$ with $1\leq i\leq m$;

• •

$S_{i}=S^{\prime}_{j}\cup S_{k}$ with $i>j>k$ and $m+1\leq i\leq 2m-1$. 2. 2.

We define the sets $S^{\prime},S^{\prime}_{1},\dots,S^{\prime}_{l}$ with $l=2m-1$ as follows:

• •

$S^{\prime}=\mathsf{Cls}(p^{h},\varphi)$;

• •

$S_{i}^{\prime}=\{s_{i}^{\prime}\}$ for $s_{i}^{\prime}\in S^{\prime}$ with $1\leq i\leq m$;

• •

$S^{\prime}_{i}=S^{\prime}_{j}\cup S^{\prime}_{k}$ with $i>j>k$ and $m+1\leq i\leq 2m-1$.

Moreover, we assume that $S^{\prime}_{i}=\bigcup{{}_{(\alpha.x.\beta,\alpha.\lnot x.\beta)\in S_{i}}\mathsf{F}^{\prime}((\alpha.x.\beta,\alpha.\lnot x.\beta))}\cap\mathsf{Cls}(p^{h},\mathsf{Cls}\varphi)$. 3. 3.

We define the sets $S^{\prime\prime},S^{\prime\prime}_{1},\dots,S^{\prime\prime}_{l}$ with $l=2m-1$ as follows:

• •

$S^{\prime\prime}=\mathsf{Cls}(p^{l},\varphi)$;

• •

$S_{i}^{\prime\prime}=\{s_{i}^{\prime\prime}\}$ for $s_{i}^{\prime\prime}\in S^{\prime\prime}$ with $1\leq i\leq m$;

• •

$S^{\prime\prime}_{i}=S^{\prime\prime}_{j}\cup S^{\prime\prime}_{k}$ with $i>j>k$ and $m+1\leq i\leq 2m-1$.

Moreover, we assume that $S^{\prime}_{i}=\bigcup{{}_{(\alpha.x.\beta,\alpha.\lnot x.\beta)\in S_{i}}\mathsf{F}^{\prime}((\alpha.x.\beta,\alpha.\lnot x.\beta))}\cap\mathsf{Cls}(p^{l},\mathsf{Cls}\varphi)$.

Let $A_{i}=S^{\prime}_{i}\cup S^{\prime\prime}_{i}$ with $1\leq i\leq 2m-1$ and ${\cal{A}}=\{A_{1},\dots,A_{2m-1}\}$. Now it follows from Lemma 4 and the definition of an OBDD that there is a set ${\overline{\cal{A}}}=\{A_{i_{1}},\dots,A_{i_{m-m^{\prime}}}\}$ such that for each $\overline{A}\in{\overline{\cal{A}}}$ there is $A\in{\cal{A}}$ such that $\overline{A}\subseteq A$. Hence, by Lemma 3 there are $m-m^{\prime}$ pairs

[TABLE]

in the set $P$, let us call this set $P^{\prime}$, such that for each $(\alpha^{\prime}.x.\beta^{\prime},\alpha^{\prime}.\lnot x.\beta^{\prime})\in P^{\prime}$ there is $(\alpha.x.\beta,\alpha.\lnot x.\beta)\in P\backslash P^{\prime}$ such that $\alpha.x.\beta,\alpha^{\prime}.x.\beta^{\prime}\not\models C$ and $\alpha.\lnot x.\beta,\alpha^{\prime}.\lnot x.\beta^{\prime}\not\models D$ for some $C,D\in\mathsf{Cls}(\varphi)$. By Corollary 2 we obtain that there is a CNF $\psi\in\mathsf{Res}(p,\varphi)$ such that $|\mathsf{Cls}(\psi)|~{}\leq~{}|\mathsf{Cls}(\varphi)|$.

It follows from Lemmas 5 and 6 that the number of resolution steps needed to simulate elimination of node $p$ is bounded by the minimum of $|\mathsf{Path^{f}}(p)|/2$ and $|\varphi)|$.

Lemma 7 below is a straightforward consequence of Lemma 6, and it somewhat relates the upper bound on the number of resolution steps simulating elimination of $p$ and the number of the $\mathsf{false}$-paths that go through the node $p$ in combination with the number of the clauses falsifying these paths (expressed by $\mathsf{\tau}(.,.)$).

Lemma 7

Let $\varphi$ be a CNF and $\mathsf{B}$ be an OBDD such that $\varphi\unlhd\mathsf{B}$. Suppose $\mathsf{B}\rightarrow_{p}\mathsf{B}^{\prime}$ for some $p\in\mathsf{Node}(\mathsf{B})$ and $\mathsf{B}^{\prime}$. Then there is a $\psi\in\mathsf{Res}(p,\varphi)$ such that

[TABLE]

Proof

We take into account that by definition of $\mathsf{\tau}(.,.)$, $|\mathsf{Path^{f}}(p)|-\mathsf{\tau}(p,\varphi)=|\mathsf{Cls}(p,\varphi)|$, and the lemma trivially holds.

4.2 Invariant

Now we will prove that although resolution steps generate new clauses, the number of resolution steps needed to simulate elimination of a node remains bounded by the number of clauses encoded by this OBDD. In fact, we demonstrate a kind of monotonicity expressed by Lemma 8.

Lemma 8

Assume a CNF $\varphi$ and an OBDD $\mathsf{B}$ with $\varphi\unlhd\mathsf{B}$. Suppose $\mathsf{B}\rightarrow_{p}\mathsf{B}^{\prime}$ and $q\rightarrow_{p}q^{\prime}$ for $p,q\in\mathsf{Node}(\mathsf{B})$ and $q^{\prime}\in\mathsf{Node}(\mathsf{B}^{\prime})$. Let $\mathsf{high}(q^{\prime})\equiv\mathsf{low}(q^{\prime})$. Then there is a $\varphi^{\prime}\in\mathsf{Res}(p,\varphi)$ such that

[TABLE]

Proof

Suppose the nodes $p$ and $q$ are not connected by a path. Then removing the node $p$ does not affect the $\mathsf{false}$-paths that go through the node $q$. That is, $\mathsf{Path^{f}}(q^{\prime})=\mathsf{Path^{f}}(q)$ and $\mathsf{\tau}(q^{\prime},\varphi\wedge\varphi^{\prime})=\mathsf{\tau}(q,\varphi)$. Hence,

[TABLE]

Now we assume that $p$ and $q$ are connected by a path. We construct $\varphi^{\prime}$ as it is defined in the proof of Lemma 5 and we consider following cases. 2. 2.

Let $q\in\mathsf{Node}(\mathsf{B}^{p})$ where $\mathsf{B}^{p}$ is the subOBDD of $\mathsf{B}$ rooted at the node $p$.

We observe that

[TABLE]

if and only if $\alpha.x.\beta\not\models C$ and $\alpha.\lnot x.\beta\not\models D$ for some $\alpha.\beta\in\mathsf{Path^{f}}(\mathsf{high}(p))$ (alternatively, we could use $\mathsf{Path^{f}}(\mathsf{low}(p))$ as $\mathsf{high}(p)\equiv\mathsf{low}(p)$) and $C\in\mathsf{Cls}(\mathsf{root}(\mathsf{high}(p)),\varphi)$, $D\in\mathsf{Cls}(\mathsf{root}(\mathsf{low}(p)),\varphi)$. Hence,

[TABLE] 3. 3.

Let $p\in\mathsf{Node}(\mathsf{B}^{q})$ where $\mathsf{B}^{q}$ is the subOBDD of $\mathsf{B}$ rooted at the node $q$.

Let $\overline{\mathsf{Path^{f}}}(p)=\mathsf{Path^{f}}(q)\backslash\mathsf{Path^{f}}(p)$. Let

[TABLE]

[TABLE]

[TABLE]

We use the same arguments as in case 1 for the clauses in ${{\cal{C}}}^{q}$, the same arguments as in case 2 for the clauses in ${{\cal{C}}}^{p}$ and apply Lemma 3 for the clauses in ${{\cal{C}}}^{q,p}$.

Lemma 9

Assume CNFs $\varphi_{1}$ and $\varphi_{2}$, and OBDDs $\mathsf{B}_{1}$ and $\mathsf{B}_{2}$ with $\varphi_{1}\unlhd\mathsf{B}_{1}$ and $\varphi_{2}\unlhd\mathsf{B}_{2}$. Let for any $q_{1}\in\mathsf{Node}(B_{1})$ and $q_{2}\in\mathsf{Node}(B_{2})$, and some $k_{1},k_{2}\geq 0$

• •

$|\mathsf{Path^{f}}(q_{1})|-\mathsf{\tau}(q_{1},\varphi_{1})\leq k_{1}$**

• •

$|\mathsf{Path^{f}}(q_{2})|-\mathsf{\tau}(q_{2},\varphi_{2})\leq k_{2}$**

Then Algorithm 1 returns the OBDD $\mathsf{B}_{1}\land\mathsf{B}_{2}$ such that for any $q\in\mathsf{Node}(\mathsf{B}_{1}\wedge\mathsf{B}_{2})$

[TABLE]

Proof

Observe that for any CNF $\varphi$ and an OBDD $\mathsf{B}$ such that $\varphi\unlhd\mathsf{B}$ and $q\in\mathsf{Node}(\mathsf{B})$,

[TABLE]

We recall that by Lemma 1, $\varphi_{1}\land\varphi_{2}\unlhd\mathsf{B}_{1}\land\mathsf{B}_{2}$ and define the sets $S_{1}$ and $S_{2}$ as follows:

• •

$S_{1}=\{\alpha\in\mathsf{Path^{f}}(\mathsf{B}_{1}\wedge\mathsf{B}_{2})\mid\mathsf{F}(\alpha)\in\mathsf{Cls}(\varphi_{1})\}$;

• •

$S_{2}=\{\alpha\in\mathsf{Path^{f}}(\mathsf{B}_{1}\wedge\mathsf{B}_{2})\mid\mathsf{F}(\alpha)\in\mathsf{Cls}(\varphi_{2})\}$.

That is, the set $S_{1}$ contains the $\mathsf{false}$-paths of $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ falsified by the clauses of $\varphi_{1}$ and $S_{2}$ contains the $\mathsf{false}$-paths of $\mathsf{B}_{1}\wedge\mathsf{B}_{2}$ falsified by the clauses of $\varphi_{2}$. Suppose

• •

$m_{1}=|S_{1}|-|\mathsf{Path^{f}}(\mathsf{root}(\mathsf{B}_{1}))|$;

• •

$m_{2}=|S_{2}|-|\mathsf{Path^{f}}(\mathsf{root}(\mathsf{B}_{2}))|$.

It follows from Lemma 1 and the definition of $\mathsf{\tau}(.,.)$ that

[TABLE]

and therefore for any $q\in\mathsf{Node}(\varphi_{1}\wedge\varphi_{2})$

[TABLE]

Now we combine the results established by Lemmas 6-9 and obtain the following corollary.

Corollary 3

Assume an unsatisfiable CNF $\varphi$. Let $\mathsf{B}_{1},\dots,\mathsf{B}_{k}$ be an OBDD refutation of $\varphi$. Then elimination of a node in any OBDD $\mathsf{B}_{i}$, $1\leq i\leq k$, can be simulated by at most $|\mathsf{Cls}(\varphi)|$ resolution steps.

Example 4

The CNFs $\mathsf{PHP}_{n}$, $n\geq 1$, formalising the pigeonhole principle is presented in Example 3. We consider the OBDD refutation of $\mathsf{PHP}_{2}$ depicted in Figure 4.

The following resolution refutation simulates removing the nodes of the OBDD $\mathsf{B}_{17}$.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

5 The Main Result

Now we establish the main result that any OBDD refutation of an unsatisfiable CNF $\varphi$ of size $n$ can be simulated by a resolution refutation of $\varphi$ of size at most $O(n^{2})$.

Theorem 5.1

Assume an unsatisfiable CNF $\varphi$. If there is an OBDD refutation of $\varphi$ of size $n$ then there is a resolution refutation of it of size $O(|\mathsf{Cls}(\varphi)|\cdot n)$.

Proof

By Corollary 3, elimination of a node can be simulated by at most $|\mathsf{Cls}(\varphi)|$ steps. Since the OBDD refutation has size $n$, we obtain that there is a resolution refutation of $\varphi$ of size $O(|\mathsf{Cls}(\varphi)|\cdot n)$.

Now, Theorem 1.1 stating that if there is an OBDD refutation of $\varphi$ of size $n$ then there is a resolution refutation of $\varphi$ of size $O(n^{2})$ follows straightforwardly from Theorem 5.1.

Proof

(Proof of Theorem 1.1) We can assume without loss of generality that $\varphi$ is a minimally unsatsfiable CNF, that is removing any clause from $\varphi$ will result in a satisfiable CNF.

Then the size of any OBDD refutation of $\varphi$ is at least $|\mathsf{Cls}(\varphi)|$, that is $|\mathsf{Cls}(\varphi)|\leq n$. By Theorem 5.1, there is a resolution refutation of $\varphi$ of size $O(k)$, where

[TABLE]

6 Conclusions

The main reason for this study comes from the interest in providing theoretical explanations of the relative efficiency of algorithms used in SAT solving.

In this paper we show that resolution simulates OBDDs polynomially if we limit both to CNFs and thus answered the open question of Groote and Zantema posed in [8] whether there exists unsatisfiable CNFs having polynomial OBDD refutations and exponentially long resolution refutations.

The goal of this study was to show the existence of such a polynomial simulation rather than provide the tightest upper bound. We envisage that an OBDD refutation can be simulated by resolution refutation with linear increase in size but it would require a more elaborated proof.

Acknowledgments

The author thanks Erika Ábrahám for helpful discussions at the early stage of this study.