An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF

Abstract

We define a distance function on propositional formulas in CNF as a measure of non-isomorphism of formulas: the larger the distance between two formulas is, the further they are from being isomorphic. This distance induces a metric on isomorphism classes of formulas. We show how this distance can be used for $\mathrm{SAT}$ solving, namely for per-instance algorithm selection where there is a “portfolio” of $\mathrm{SAT}$ solvers and there is a “meta-solver” that chooses a solver from the portfolio for a given input formula.

1. Introduction

Two propositional formulas in CNF are isomorphic if one of them can be obtained from the other by renaming variables and flipping literals. It is natural to view isomorphism as “similarity” of formulas, but this similarity measure is all or nothing: any two formulas are similar or not. How can we modify this measure to make it gradual? In this paper, we define a distance functions on formulas such that the smaller the distance between two formulas is, the closer they are to being isomorphic. This distance function is a pseudometric on formulas and, thereby, it induces a metric on isomorphism classes of formulas.

Application to $\mathrm{SAT}$ Solving. Before we describe the distance function and its properties, we briefly note how this distance can be used for $\mathrm{SAT}$ solving, see more details in this section below and a formal description in Sections 5 and 6. We consider the following variant of per-instance algorithm selection [11]. There are a “dataset” D of formulas and a “portfolio” P of $\mathrm{SAT}$ algorithms such that for every formula $\mathrm{\varphi }\in D$ , at least one algorithm in P performs fast on ϕ. There is a “meta-algorithm” S that takes a formula ψ as input and tries to select an algorithm from P that performs fast on ψ. How does S work?

Under certain conditions on D and P (we specify these conditions in Section 6), if an algorithm from P performs fast on a formula $\mathrm{\varphi }\in D$ then this algorithm performs fast on any formula close to ϕ. This suggests that S finds a formula $\mathrm{\varphi }\in D$ closest to ψ and selects an algorithm $A\in P$ that performs fast on ϕ. If the distance between ψ and ϕ is small enough, then A performs fast on ψ as well. Otherwise (D contains no formula close to ψ), the meta-algorithm S gives up and returns “can’t select”.

Distance Function. Precise definitions are given in Sections 2 and 3; here we give the main idea. The distance between two formulas is defined by combining isomorphism of formulas and symmetric difference of sets. Let ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ be propositional formulas in CNF ( ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ are sets of clauses). The distance between them, denoted $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ , is the minimum cardinality of the symmetric differences of formulas ${\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2^{\prime }$ , where the minimum is taken over all formulas ${\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2^{\prime }$ such that they are isomorphic to ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ respectively. This definition has two equivalent forms:

$\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ is the minimum number of clauses that can be removed from ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ so that the remaining subformulas are isomorphic to each other;

$\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ is the minimum number of clauses that can be added to ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ so that the resulting superformulas are isomorphic to each other.

By definition, δ is preserved under isomorphism: if ${\mathrm{\varphi }}_1$ , ${\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2$ , ${\mathrm{\varphi }}_2^{\prime }$ are pairs of isomorphic formulas, then $$\begin{array}{c}\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=\mathrm{\delta }({\mathrm{\varphi }}_1^{\prime },{\mathrm{\varphi }}_2^{\prime }).\end{array}$$ In Section 3, we show that δ is a pseudometric on formulas. This pseudometric induces a metric on isomorphism classes of formulas.

Note that this approach to defining a distance function is essentially a replica of the approach used by Gromov in the definition of the Gromov–Hausdorff distance on metric spaces [5,10]. The Gromov–Hausdorff distance between metric spaces $M_1$ and $M_2$ is the minimum Hausdorff distance between the images of $M_1$ and $M_2$ under distance-preserving functions $f_1$ and $f_2$ from these spaces to a metric space M, where the minimum is taken over all M, $f_1$ , and $f_2$ .

Computing the Distance. In Section 4 we address the problem of computing the distance function δ. Although it is $\mathsf{NP}$ -hard to compute $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ in general, it is easier to determine whether this distance is “small”. Namely, for every integer d, the problem of verifying the equality $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=d$ is Turing reducible to the graph isomorphism problem. The latter can be solved in quasi-polynomial time [4] and, in practice, it is often solved efficiently using Nauty tools [14].

What distance is computed in the per-instance algorithm selection approach described above? The meta-algorithm determines whether the dataset contains a formula lying within a small distance from the input formula ψ. Assuming that a “small distance” means a constant distance, this can be done by a polynomial-time oracle algorithm with an oracle for graph isomorphism.

Per-Instance Algorithm Selection. Section 6 shows how the distance δ can be used for per-instance algorithm, see the brief sketch above. The meta-algorithm S defined in this section is called the fixed-distance selector. Taking a formula ψ and an integer d as input, S checks whether the dataset D contains a formula ϕ such that $\mathrm{\delta }(\mathrm{\varphi },\mathrm{\psi })⩽d$ . If so, S selects an algorithm $A\in P$ that performs fast on ϕ and returns it. Otherwise, S says “can’t select”. We formulate conditions on D and P that guarantee fast performance of A on the input formula ψ.

The key point of this approach is that every algorithm $A\in P$ has the following property:

If A performs fast on a formula ϕ, then A performs fast on any formula close to ϕ.

To formalize this property, we define a class of parameters of formulas that we call parameters of constant variation (Section 5). By a parameter we mean any computable function from the set of formulas to the non-negative integers. A parameter π is a parameter of constant variation if the following holds:

• π is preserved under isomorphism;

• for every formula ϕ, a slight variation of ϕ can cause only a slight change of $\mathrm{\pi }(\mathrm{\varphi })$ : the addition of one clause to ϕ can change $\mathrm{\pi }(\mathrm{\varphi })$ by only a constant value that does not depend on ϕ.

The class of constant-variation parameters includes incidence treewidth, maximum deficiency, and many other parameters π such that the parameterized problem $\mathrm{SAT}(\mathrm{\pi })$ is fixed-parameter tractable [15]. This class can be characterized in terms of the distance δ. Namely, π is a parameter of constant variation if and only if $$\begin{array}{c}|\mathrm{\pi }({\mathrm{\varphi }}_1)\mathbf{-}\mathrm{\pi }({\mathrm{\varphi }}_2)|⩽c\mathbf{\cdot }\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)\end{array}$$ for some number c and all formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ . This characterization connects the running time of parameterized algorithms from the portfolio P with the distance δ.

Extension to CSP Instances. In Section 7 we briefly discuss an extension of the distance function δ from CNF formulas to instances of the constraint satisfaction problem.

2. Formulas and Isomorphism

Propositional Formulas in CNFs. A literal is a propositional variable or its negation; each of them is the complement of the other. The complement of a literal a is denoted by $\neg a$ . A clause is a nonempty finite set of literals that contains no pair of complements. A propositional formula in Conjunctive Normal Form, called a formula or CNF formula for short, is a finite set of clauses.

Let ϕ be a formula. We write $|\mathrm{\varphi }|$ to denote the number of clauses of ϕ and we write $var(\mathrm{\varphi })$ to denote the set of variables appearing in ϕ (with or without negation). The width of a clause C is the number of literals in C. If ψ is a formula such that $\mathrm{\varphi }\subseteq \mathrm{\psi }$ , we call ϕ a subformula of ψ.

An assignment for a formula ϕ is a function from $var(\mathrm{\varphi })$ to $\{0,1\}$ . Let α be such an assignment and $x\in var(\mathrm{\varphi })$ . We say that x is true under α if $\mathrm{\alpha }(x)=1$ ; otherwise x is false under α. Symmetrically, we say that $\neg x$ is true under α if $\mathrm{\alpha }(x)=0$ ; otherwise $\neg x$ is false under α. A clause is thought of as the disjunction of its literals; we say that α satisfies a clause $C\in \mathrm{\varphi }$ if at least one literal in C is true under α. A formula is thought of as the conjunction of its clauses; if α satisfies all clauses of ϕ then we say that α satisfies ϕ and call α a satisfying assignment for ϕ. The empty formula, denoted by ⊤, is considered to be satisfied by any assignment. The number of satisfying assignments for ϕ is denoted by $\mathrm{\#}\mathrm{\varphi }$ [9].

We write $\mathrm{SAT}$ to denote the satisfiability problem for propositional formulas in CNF: given a formula, does it have a satisfying assignment? The counting version of $\mathrm{SAT}$ , denoted by $\mathrm{\#}\mathrm{SAT}$ , is the following function problem: given a formula ϕ, find $\mathrm{\#}\mathrm{\varphi }$ .

Isomorphisms. Informally, two formulas are isomorphic if one of them can be obtained from the other by renaming variables and flipping literals. A more formal definition is given below.

Let ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ be formulas. Let $L_1$ and $L_2$ be the sets of literals defined by $$\begin{array}{l}{L}_1=var({\mathrm{\varphi }}_1)\mathbf{\cup }\{\neg x\mid x\in var({\mathrm{\varphi }}_1)\}\\ L_2=var({\mathrm{\varphi }}_2)\mathbf{\cup }\{\neg x\mid x\in var({\mathrm{\varphi }}_2)\}\end{array}$$ Let f be a bijection from $L_1$ to $L_2$ . We call f an isomorphism from ${\mathrm{\varphi }}_1$ to ${\mathrm{\varphi }}_2$ if the following holds:

f and its inverse preserve the complement relation, which means that for all literals $a,b\in L_1$ , $$\begin{array}{c}a\text{is the complement of}b\iff f(a)\text{is the complement of}f(b);\end{array}$$

f and its inverse preserve the clauses, which means that for all literals $a_1,\dots ,a_k\in L_1$ , $$\begin{array}{c}\{a_1,\dots ,a_k\}\text{is a clause of}{\mathrm{\varphi }}_1\iff \{f(a_1),\dots ,f(a_k)\}\text{is a clause of}{\mathrm{\varphi }}_2.\end{array}$$

Formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ are isomorphic, written as ${\mathrm{\varphi }}_1\simeq {\mathrm{\varphi }}_2$ , if there is an isomorphism from ${\mathrm{\varphi }}_1$ to ${\mathrm{\varphi }}_2$ . For every formula ϕ, we write $[\mathrm{\varphi }]$ to denote the isomorphism class of ϕ, i.e., the set of all formulas isomorphic to ϕ. Thus, $[\mathrm{\varphi }]$ can be viewed as ϕ up to isomorphism. Note that an isomorphism between formulas is sometimes defined using renamings only [3], yet in this paper we adhere to the more general version.

3. Distance Function on Formulas

Let X be a set. A function d from $X\mathbf{\times }X$ to ${\mathbb{R}}_{⩾0}$ is a distance function if $d(x,y)=d(y,x)$ and $d(x,x)=0$ for all $x,y\in X$ . Consider the following two conditions on d: for all $x,y,z\in X$ ,

(1)

if $d(x,y)=0$ then $x=y$ ;

(2)

$d(x,y)⩽d(x,z)\mathbf{+}d(z,y)$ (triangle inequality).

The distance function d is a metric on X if d satisfies both (1) and (2). If d satisfies (2), but not necessarily (1), then d is a pseudometric on X.

To define a distance function on formulas, we recall the notation for the symmetric difference operation. The symmetric difference of sets A and B is denoted by $A\mathbf{△}B$ : $$\begin{array}{c}A\mathbf{△}B=(A\mathbf{\setminus }B)\mathbf{\cup }(B\mathbf{\setminus }A)=(A\mathbf{\cup }B)\mathbf{\setminus }(A\mathbf{\cap }B).\end{array}$$

Definition 1.

Let δ be the following function that maps pairs of CNF formulas to nonnegative integers: $$\begin{array}{c}\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=\underset{{\mathrm{\varphi }}_1^{\prime },{\mathrm{\varphi }}_2^{\prime }}{min}|{\mathrm{\varphi }}_1^{\prime }\mathbf{△}{\mathrm{\varphi }}_2^{\prime }|\end{array}$$ where the minimum is taken over all formulas ${\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2^{\prime }$ such that ${\mathrm{\varphi }}_1^{\prime }\simeq {\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2^{\prime }\simeq {\mathrm{\varphi }}_2$ .

Proposition 1.

The distance function δ is a pseudometric.

Proof: Consider the distance function $d_{\mathbf{△}}$ on finite sets defined as follows: for all finite sets A and B, $$\begin{array}{c}{d}_{\mathbf{△}}(A,B)=|A\mathbf{△}B|.\end{array}$$ It is well known that $d_{\mathbf{△}}$ is a metric. Indeed, we have $$\begin{array}{c}(A\mathbf{△}B)\mathbf{△}(B\mathbf{△}C)=A\mathbf{△}C\end{array}$$ and, hence, the triangle inequality for $d_{\mathbf{△}}$ holds. Now the triangle inequality for δ follows from the triangle inequality for $d_{\mathbf{△}}$ .  □

Suprema and Infima. We say that a formula ϕ is embedded into a formula ψ if ϕ is isomorphic to some subformula of ψ. A formula ψ is called a supremum of formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ if the following holds:

both ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ are embedded into ψ;

for every formula ${\mathrm{\psi }}^{\prime }$ such that both ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ are embedded into ${\mathrm{\psi }}^{\prime }$ , we have $|\mathrm{\psi }|⩽|{\mathrm{\psi }}^{\prime }|$ .

Similarly, we say that a formula 𝜃 is an infimum of formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ if

• 𝜃 is embedded into both ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ ;

• for every formula ${\mathrm{𝜃}}^{\prime }$ such that 𝜃 is embedded into both ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ , we have $|\mathrm{𝜃}|⩾|{\mathrm{𝜃}}^{\prime }|$ .

Proposition 2.

Let ψ and 𝜃 be respectively a supremum and an infimum of formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ . Then $$\begin{array}{}\text{(1)}& \mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=|\mathrm{\psi }|\mathbf{-}|\mathrm{𝜃}|;\text{(2)}& \mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=2|\mathrm{\psi }|\mathbf{-}|{\mathrm{\varphi }}_1|\mathbf{-}|{\mathrm{\varphi }}_2|;\text{(3)}& \mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=|{\mathrm{\varphi }}_1|\mathbf{+}|{\mathrm{\varphi }}_2|\mathbf{-}2|\mathrm{𝜃}|.\end{array}$$

Proof: It straightforwardly follows from the definition of δ and properties of the symmetric difference.  □

Induced Metric on Isomorphism Classes. It follows from the definition of δ that if ${\mathrm{\varphi }}_1\simeq {\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2\simeq {\mathrm{\varphi }}_2^{\prime }$ , then $$\begin{array}{c}\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=\mathrm{\delta }({\mathrm{\varphi }}_1^{\prime },{\mathrm{\varphi }}_2^{\prime }).\end{array}$$ Thus, δ induces a distance function on isomorphism classes of formulas: this function, denoted by Δ, is defined by $$\begin{array}{c}\Delta ([{\mathrm{\varphi }}_1],[{\mathrm{\varphi }}_2])=\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2).\end{array}$$ Proposition 1 implies that Δ is a metric on the set of isomorphism classes.

Example. Let ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ be the following formulas: $$\begin{array}{l}{\mathrm{\varphi }}_1=\{\{x_1,\neg x_4\},\{x_2,\neg x_3\},\{\neg x_1,\neg x_2,x_4\}\};\\ {\mathrm{\varphi }}_2=\{\{y_1,\neg y_2,y_3\},\{\neg y_1,y_2\},\{y_3,y_4,\neg y_5\},\{\neg y_4\}\}.\end{array}$$ Consider the following subformula of ${\mathrm{\varphi }}_1$ : $$\begin{array}{c}\mathrm{𝜃}=\{\{x_1,\neg x_4\},\{\neg x_1,\neg x_2,x_4\}\}.\end{array}$$ The formula 𝜃 is isomorphic to the following subformula of ${\mathrm{\varphi }}_2$ : $$\begin{array}{c}\{\{y_1,\neg y_2,y_3\},\{\neg y_1,y_2\}\}\end{array}$$ (this isomorphism is given by $x_1\mapsto \neg y_1$ , $x_2\mapsto \neg y_3$ , $x_4\mapsto \neg y_2$ ). Thus, 𝜃 is embedded into both ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ . It is easy to check that no formula with more than two clauses is embedded into ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ . Hence, 𝜃 is an infimum of ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ . Using Proposition 2, namely equality (3), we can find the distance between ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ : $$\begin{array}{c}\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=|{\mathrm{\varphi }}_1|\mathbf{+}|{\mathrm{\varphi }}_2|\mathbf{-}2|\mathrm{𝜃}|=3\mathbf{+}4\mathbf{-}2\mathbf{\cdot }2=3.\end{array}$$

The distance can also be found using a supremum. Consider the following formula that contains ${\mathrm{\varphi }}_2$ as a subformula: $$\begin{array}{c}\mathrm{\psi }=\{\{y_1,\neg y_2,y_3\},\{\neg y_1,y_2\},\{y_3,y_4,\neg y_5\},\{\neg y_4\},\{\neg y_3,\neg y_4\}\}.\end{array}$$ The formula ${\mathrm{\varphi }}_1$ is embedded into ψ with the isomorphism given by $x_1\mapsto \neg y_1$ , $x_2\mapsto \neg y_3$ , $x_3\mapsto y_4$ , $x_4\mapsto \neg y_2$ . Since ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ cannot be embedded into a formula with less than five clauses, ϕ is a supremum of ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ . By equality (2), we have $$\begin{array}{c}\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=2|\mathrm{\psi }|\mathbf{-}|{\mathrm{\varphi }}_1|\mathbf{-}|{\mathrm{\varphi }}_2|=2\mathbf{\cdot }5\mathbf{-}3\mathbf{-}4=3.\end{array}$$

4. Distance Computation

Given formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ , how hard is it to compute $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ ? We show that the problem of computing the distance δ is at least as hard as the hardest problems in $\mathsf{NP}$ . On the positive side, this general problem can be restricted to a more tractable case: determine whether the distance $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ is “small”, where “small” means a constant not depending on the input formulas.

To make these claims more precise and to prove them, we consider the following computational problems:

• The embedding problem: given formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ , determine whether ${\mathrm{\varphi }}_1$ is embedded into ${\mathrm{\varphi }}_2$ .

• The distance verification problem: given formulas ${\mathrm{\varphi }}_1$ , ${\mathrm{\varphi }}_2$ , and an integer d, determine whether $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=d$ .

• The distance computation problem: given formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ , find the distance $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ .

Proposition 3.

The embedding problem is $\mathsf{NP}$ -complete.

Proof: It is obvious that the embedding problem is in $\mathsf{NP}$ . To prove the completeness, we reduce the Hamiltonian path problem to the embedding problem. Without loss of generality, we can assume that instances of the Hamiltonian path problem are graphs without isolated vertices.

In our reduction, every graph G without isolated vertices is represented by a formula denoted by ${\mathrm{\varphi }}_G$ and defined as follows. Let G be a graph on vertices $v_1,\dots ,v_n$ and with edges $e_1,\dots ,e_m$ . The formula ${\mathrm{\varphi }}_G$ has $n\mathbf{+}m$ variables $$\begin{array}{c}{x}_1,\dots ,x_n,y_1,\dots ,y_m\end{array}$$ where each $x_i$ represents the vertex $v_i$ and each $y_k$ represents the edge $e_k$ . Using these variables, we form m clauses of ${\mathrm{\varphi }}_G$ : for each edge $e_k$ with endpoints $v_i$ and $v_j$ , there is the clause $\{y_k,x_i,x_j\}$ . Note that the map $G\mapsto {\mathrm{\varphi }}_G$ has the following property: for all graphs G and H without isolated vertices, H is isomorphic to a subgraph of G if and only if ${\mathrm{\varphi }}_H$ is embedded into ${\mathrm{\varphi }}_G$ .

Now we define a reduction of the Hamiltonian path problem to the embedding problem as follows. Let G be a graph with n vertices (all of them are non-isolated) and m edges. Let H be a Hamiltonian path on n vertices: a graph on vertices $u_1,\dots ,u_n$ with edges between $u_i$ and $u_{i\mathbf{+}1}$ where $i=1,\dots ,n\mathbf{-}1$ . The reduction maps G to the pair $({\mathrm{\varphi }}_H,{\mathrm{\varphi }}_G)$ . It is easy to see that G has a Hamiltonian path if and only if H is isomorphic to a subgraph of G. Therefore, G has a Hamiltonian path if and only if ${\mathrm{\varphi }}_H$ is embedded into ${\mathrm{\varphi }}_G$ . It remains to note that the pair $({\mathrm{\varphi }}_H,{\mathrm{\varphi }}_G)$ can be computed from G in polynomial time.  □

Proposition 4.

The distance verification problem is $\mathsf{NP}$ -hard.

Proof: We show that the embedding problem is reducible to the distance verification problem. The reduction is a polynomial-time algorithm that takes an instance $({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ of the embedding problem as input and outputs the equality $$\begin{array}{}\text{(4)}& \mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=|{\mathrm{\varphi }}_2|\mathbf{-}|{\mathrm{\varphi }}_1|.\end{array}$$ If ${\mathrm{\varphi }}_1$ is embedded into ${\mathrm{\varphi }}_2$ then $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=|{\mathrm{\varphi }}_2|\mathbf{-}|{\mathrm{\varphi }}_1|$ by Proposition 2 and, hence, (4) holds.

Conversely, suppose that (4) holds. By Definition 1, $$\begin{array}{c}\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=|{\mathrm{\varphi }}_1^{\prime }\mathbf{△}{\mathrm{\varphi }}_2^{\prime }|\end{array}$$ for some formulas ${\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2^{\prime }$ such that ${\mathrm{\varphi }}_1^{\prime }\simeq {\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2^{\prime }\simeq {\mathrm{\varphi }}_2$ . Hence, using (4), we obtain $$\begin{array}{c}|{\mathrm{\varphi }}_1^{\prime }\mathbf{△}{\mathrm{\varphi }}_2^{\prime }|=\left|{\mathrm{\varphi }}_1^{\prime }\right|\mathbf{-}\left|{\mathrm{\varphi }}_2^{\prime }\right|.\end{array}$$ By properties of the symmetric difference, the latter equality holds only if ${\mathrm{\varphi }}_1^{\prime }$ is a subformula of ${\mathrm{\varphi }}_2^{\prime }$ . Therefore, ${\mathrm{\varphi }}_1$ is embedded into ${\mathrm{\varphi }}_2$ , which completes the proof.  □

Corollary 5.

The distance computation problem is at least as hard as the hardest problems in $\mathsf{NP}$ .

Proof: There is a trivial polynomial-time Turing reduction of the distance verification problem (shown to be $\mathsf{NP}$ -hard) to the distance computation problem.  □

Proposition 6.

The distance verification problem can be solved by an oracle algorithm A with the following properties:

the oracle of A answers questions of whether two given formulas are isomorphic;

there exists a polynomial p such that on every instance $({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2,d)$ , the running time of A is at most $p(s)\mathbf{\cdot }{M}^d$ , where s is the size of the instance and $M=max(|{\mathrm{\varphi }}_1|,|{\mathrm{\varphi }}_2|)$ .

Proof: The distance verification problem can be solved using the equivalent definitions of δ given by Proposition 2. For instance, we can use equality (3) that expresses δ in terms of infima: $$\begin{array}{c}\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=|{\mathrm{\varphi }}_1|\mathbf{+}|{\mathrm{\varphi }}_2|\mathbf{-}2|\mathrm{𝜃}|\end{array}$$ where 𝜃 is an infimum of ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ . In fact, this definition shows that distance verification is equivalent to “infimum verification”: $$\begin{array}{c}\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=d\iff |\mathrm{𝜃}|={\displaystyle \frac{|{\mathrm{\varphi }}_1|\mathbf{+}|{\mathrm{\varphi }}_2|\mathbf{-}d}{2}}\end{array}$$ That is, instead of verifying whether $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=d$ , we can verify whether ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ have an infimum 𝜃 that contains k clauses where $$\begin{array}{c}k={\displaystyle \frac{|{\mathrm{\varphi }}_1|\mathbf{+}|{\mathrm{\varphi }}_2|\mathbf{-}d}{2}}.\end{array}$$ The algorithm A takes $({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2,d)$ as input and uses brute force to check whether such an infimum exists. Namely, A takes the following two steps.

First, A enumerates pairs $({\mathrm{𝜃}}_1,{\mathrm{𝜃}}_2)$ , where ${\mathrm{𝜃}}_1$ is a k-subset of ${\mathrm{\varphi }}_1$ and ${\mathrm{𝜃}}_2$ is a k-subset of ${\mathrm{\varphi }}_2$ . For each such pair, A asks the oracle whether ${\mathrm{𝜃}}_1$ and ${\mathrm{𝜃}}_2$ are isomorphic. If the oracle’s answer is positive, an infimum of cardinality at least k exists. The number of queries to the oracle is estimated by $$\begin{array}{cc}\hfill \left(\genfrac{}{}{0.0pt}{}{|{\mathrm{\varphi }}_1|}{k}\right)\mathbf{\cdot }\left(\genfrac{}{}{0.0pt}{}{|{\mathrm{\varphi }}_2|}{k}\right)& =\left(\genfrac{}{}{0.0pt}{}{|{\mathrm{\varphi }}_1|}{|{\mathrm{\varphi }}_1|\mathbf{-}k}\right)\mathbf{\cdot }\left(\genfrac{}{}{0.0pt}{}{|{\mathrm{\varphi }}_2|}{|{\mathrm{\varphi }}_2|\mathbf{-}k}\right)\hfill \\ \hfill & ⩽M^{|{\mathrm{\varphi }}_1|\mathbf{-}k}\mathbf{\cdot }{M}^{|{\mathrm{\varphi }}_2|\mathbf{-}k}=M^{|{\mathrm{\varphi }}_1|\mathbf{+}|{\mathrm{\varphi }}_2|\mathbf{-}2k}=M^d.\hfill \end{array}$$ Second, in a similar way, A checks whether there exist a $(k\mathbf{+}1)$ -subset of ${\mathrm{\varphi }}_1$ and a $(k\mathbf{+}1)$ -subset of ${\mathrm{\varphi }}_2$ such that these subsets are isomorphic. If no such subsets exist, there is an infimum of cardinality k. The total number of queries to the oracle in the two steps does not exceed $2M^d$ , and each query is processed in polynomial time. Therefore, the overall running time is at most $p(s)\mathbf{\cdot }{M}^d$ for some polynomial p.  □

The algorithm in Proposition 6 uses an oracle for deciding the formula isomorphism problem (given two formulas, are they isomorphic?). It is well known that this problem is polynomially equivalent to the graph isomorphism problem [3]. It is easy to modify the algorithm A so that its oracle for the formula isomorphism problem can be replaced with an oracle for the graph isomorphism problem. Let $A_G$ be the modified algorithm; the running time of $A_G$ remains the same as up to a polynomial factor.

The complexity class $\mathsf{GI}$ consists of problems that have polynomial-time Turing reduction to the graph isomorphism problem, see for example [12]. It is known that the graph isomorphism problem can be solved in quasi-polynomial time [4] and, in practice, it is often solved efficiently using Nauty tools [14].

Proposition 7.

For every integer d, the restriction of the distant verification problem to instances $({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2,d)$ is in $\mathsf{GI}$ .

Proof: For each restriction, the algorithm $A_G$ described above is a polynomial-time Turing reduction to the graph isomorphism problem.  □

5. Parameters of Constant Variation

By a parameter of formulas we mean any computable function from the set of formulas to the non-negative integers. Natural examples of parameters are the number of clauses, the number of variables, and the number of satisfying assignments. In this section we define a class of parameters of constant variation. This type of parameters is needed for the next section where we describe how the distance δ can be used for $\mathrm{SAT}$ solving. We give only two examples of constant-variation parameters, namely incidence treewidth and maximum deficiency, but many parameters for which the corresponding parameterized version of $\mathrm{SAT}$ is fixed-parameter tractable are parameters of constant variation.

Definition 2 (parameter of constant variation).

We say that a parameter π is a parameter of constant variation if it has the following two properties:

for all formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ , if ${\mathrm{\varphi }}_1\simeq {\mathrm{\varphi }}_2$ then $\mathrm{\pi }({\mathrm{\varphi }}_1)=\mathrm{\pi }({\mathrm{\varphi }}_2)$ ;

there exists a number c such that for every formula ϕ and every formula ${\mathrm{\varphi }}^{\prime }$ obtained from ϕ by adding one clause, we have $$\begin{array}{}\text{(5)}& \left|\mathrm{\pi }\right({\mathrm{\varphi }}^{\prime })\mathbf{-}\mathrm{\pi }(\mathrm{\varphi })|⩽c.\end{array}$$

The number c is called a bound on the change.

Thus, π is a parameter of constant variation if it is preserved under isomorphism and the addition of one clause to ϕ can change $\mathrm{\pi }(\mathrm{\varphi })$ by only a constant value that does not depend on ϕ. The number of clauses in a formula is a trivial example of parameters of constant variation. As for the number of variables, it is not a parameter of constant variation. Indeed, consider formulas ϕ and ${\mathrm{\varphi }}^{\prime }$ where ${\mathrm{\varphi }}^{\prime }$ is obtained from ϕ by adding one clause with arbitrarily many new variables. Then there is no constant upper bound on the difference between $|var({\mathrm{\varphi }}^{\prime })|$ and $|var(\mathrm{\varphi })|$ .

For more illustration of the notion of constant-variation parameters, we give two examples: incidence treewidth and maximum deficiency. Both parameters are well known in connection with fixed-parameter tractability of $\mathrm{SAT}$ .

Incidence Treewidth. For every formula ϕ, the incidence graph of ϕ is a bipartite graph G defined as follows. The set of vertices of G is partitioned into two subsets: one of them is the set of variables of ϕ and the other is the set of clauses of ϕ. There are only edges between variables and clauses: a variable x is connected by an edge with a clause C if and only if $x\in var(C)$ . The treewidth of the incidence graph of ϕ is called the incidence treewidth of ϕ and is denoted by $tw(\mathrm{\varphi })$ .

There are various algorithms that solve $\mathrm{SAT}$ and $\mathrm{\#}\mathrm{SAT}$ when an input formula is given along with a tree decomposition of its incidence graph. For example, the algorithm from [16] solves $\mathrm{\#}\mathrm{SAT}$ in time $2^w\mathbf{\cdot }poly(l)$ where w is the width of the input tree decomposition and l is the size of the input. Also there are algorithms that build a tree decomposition of a given graph. One of such algorithm is given in [1]: it approximates a tree decomposition with the minimum width. The combination of these two algorithms solves $\mathrm{\#}\mathrm{SAT}$ in time $2^{3.7\mathbf{\cdot }tw(\mathrm{\varphi })}\mathbf{\cdot }poly(l)$ .

Proposition 8.

Incidence treewidth is a parameter of constant variation.

Proof: If two formulas are isomorphic then their incidence graphs are isomorphic too and, therefore, incidence treewidth is preserved under isomorphism. We prove that incidence treewidth has the second property from Definition 2 with $c=1$ : for every formula ϕ and every formula ${\mathrm{\varphi }}^{\prime }$ obtained from ϕ by adding one clause, we have $tw({\mathrm{\varphi }}^{\prime })\mathbf{-}tw(\mathrm{\varphi })⩽1$ .

Consider a tree decomposition of the incidence graph of ϕ: a labeled tree T in which every vertex is labeled by a bag of vertices. We show how to extend it to a tree decomposition of the incidence graph of ${\mathrm{\varphi }}^{\prime }$ . Let C be the “new” clause added to ϕ and let $x_1,\dots ,x_k$ be the “new” variables, i.e., the variables appearing in C and not occurring in ϕ. These “new” elements must be added to T. The variables $x_1,\dots ,x_k$ are added in a simple way: (1) select any leaf of T, (2) connect it with k new vertices, and (3) assign one-element bags $\{x_1\},\dots ,\{x_k\}$ to the new vertices. Finally, we extend all bags (including the bags of new vertices) by adding the clause C.

It is easy to see that the result of our extension, the labeled tree $T^{\prime }$ , is a tree decomposition of the incidence graph of ${\mathrm{\varphi }}^{\prime }$ . Moreover, by our construction, we have $w^{\prime }\mathbf{-}w=1$ where w and $w^{\prime }$ are the width of T and the width of $T^{\prime }$ respectively. Taking the tree decomposition T such that $w=tw(\mathrm{\varphi })$ and using the obvious inequality $tw({\mathrm{\varphi }}^{\prime })⩽w^{\prime }$ , we obtain $$\begin{array}{c}tw\left({\mathrm{\varphi }}^{\prime }\right)\mathbf{-}tw(\mathrm{\varphi })⩽w^{\prime }\mathbf{-}w=1,\end{array}$$ which completes the proof.  □

Maximum Deficiency. The parameter of formulas called maximum deficiency was introduced in [8]; it relates satisfiability of a formula with matchings in its incidence graph.

Let ϕ be a formula and let M be a matching in its incidence graph. For each edge in M that connects a variable x and a clause C, we can assign x a truth value that makes C true. Therefore, if all clauses of ϕ are matched by M then ϕ is satisfiable. The maximum deficiency of a formula ϕ, denoted by $md(\mathrm{\varphi })$ , is the number of clauses unmatched by a maximum matching in the incidence graph of ϕ (this number remains the same whatever maximum matching is taken). Since a maximum matching can be found in polynomial time, $md(\mathrm{\varphi })$ is computable in polynomial time. Equivalently, due to Hall’s marriage theorem, maximum deficiency can be defined as follows: $$\begin{array}{c}md(\mathrm{\varphi })=\underset{{\mathrm{\varphi }}^{\prime }\subseteq \mathrm{\varphi }}{max}\left(\right|{\mathrm{\varphi }}^{\prime }|\mathbf{-}|var\left({\mathrm{\varphi }}^{\prime }\right)\left|\right)\end{array}$$ where the maximum is taken over all subformulas of ϕ. Note that $md(\mathrm{\varphi })⩾0$ for all ϕ because ⊤ is a subformula of every formula. The satisfiability problem parameterized by maximum deficiency is fixed-parameter tractable: the algorithms in [7,17] solve $\mathrm{SAT}$ in time $2^{md(\mathrm{\varphi })}\mathbf{\cdot }poly(l)$ where l is the size of ϕ.

Proposition 9.

Maximum deficiency is a parameter of constant variation.

Proof: First, maximum deficiency is preserved under isomorphism. Second, it is obvious that the addition of one clause to a formula ϕ can increase $md(\mathrm{\varphi })$ by at most one and, therefore, the second property from Definition 2 holds with $c=1$ .  □

Characterization in Terms of Distance. The proposition below gives an equivalent definition of parameters of constant variation in terms of the distance δ.

Proposition 10.

The following two statements are equivalent:

• (1)

A parameter π is a parameter of constant variation and c is a bound on the change.

(2)

Let π be a parameter and let c be a number such that for all formulas ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ , $$\begin{array}{}\text{(6)}& |\mathrm{\pi }({\mathrm{\varphi }}_1)\mathbf{-}\mathrm{\pi }({\mathrm{\varphi }}_2)|⩽c\mathbf{\cdot }\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2).\end{array}$$

Proof: First, suppose that (6) holds. Then $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=0$ implies $\mathrm{\pi }({\mathrm{\varphi }}_1)=\mathrm{\pi }({\mathrm{\varphi }}_2)$ , which means that π is preserved under isomorphism. If ${\mathrm{\varphi }}_2$ is obtained from ${\mathrm{\varphi }}_1$ by adding one clause, then $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=1$ and, therefore, we have the second property from Definition 2: $$\begin{array}{c}|\mathrm{\pi }({\mathrm{\varphi }}_2)\mathbf{-}\mathrm{\pi }({\mathrm{\varphi }}_1)|⩽c.\end{array}$$

Second, suppose that π is a parameter of constant variation and c is a bound on the change. Let ${\mathrm{\varphi }}_1$ and ${\mathrm{\varphi }}_2$ be arbitrary formulas. By the definition of δ and Proposition 2, there exist four formulas ${\mathrm{\varphi }}_1^{\prime }$ , ${\mathrm{\varphi }}_2^{\prime }$ , ψ, 𝜃 such that

${\mathrm{\varphi }}_1\simeq {\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2\simeq {\mathrm{\varphi }}_2^{\prime }$ ;

𝜃 is subformula of both ${\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2^{\prime }$ ;

both ${\mathrm{\varphi }}_1^{\prime }$ and ${\mathrm{\varphi }}_2^{\prime }$ are subformulas of ψ;

$\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)=|\mathrm{\psi }|\mathbf{-}|\mathrm{𝜃}|$ .

Thus, ψ is obtained from 𝜃 by the addition of $\mathrm{\delta }({\mathrm{\varphi }}_1,{\mathrm{\varphi }}_2)$ clauses. Since the addition of one clause can change $\mathrm{\pi }(\mathrm{𝜃})$ by at most c, we have inequality (6).  □

Note that inequality (6) is the same as in the definition of Lipschitz functions (also called Lipschitz continuous functions or Lipschitz maps) [5]. Thus, loosely speaking, π is a parameter of constant variation if and only if π is a Lipschitz function.

6. Fixed-Distance Selector

There are many techniques for designing a “meta-algorithm” that solves $\mathrm{SAT}$ using a given “portfolio” of $\mathrm{SAT}$ algorithms [11]. We show how the distance δ can be used in a variant of the per-instance algorithm selection technique. Namely, we describe an incomplete meta-algorithm, called a fixed-distance selector, that takes a formula ψ as input and tries to select an algorithm from the portfolio that performs fast on ψ. Then we formulate conditions on portfolios and prove that if the conditions are met then the selected algorithm indeed performs efficiently on ψ.

Datasets and Portfolios. We consider algorithms that take formulas as inputs, for example, algorithms that solve $\mathrm{SAT}$ , or $\mathrm{\#}\mathrm{SAT}$ , or $\mathrm{MAXSAT}$ . Let D be a finite set of formulas called a dataset. With every formula $\mathrm{\varphi }\in D$ , we associate a non-empty finite set $E_{\mathrm{\varphi }}$ of algorithms that perform fast on ϕ (we do not define here what “fast” means, this will be done in the conditions formulated below). Note that sets $E_{\mathrm{\varphi }}$ associated with different formulas may or may not overlap. Given a dataset D, the set $$\begin{array}{c}P={\displaystyle \bigcup }_{\mathrm{\varphi }\in D}{E}_{\mathrm{\varphi }}\end{array}$$ of algorithms is called the portfolio corresponding to D. Thus, for every formula $\mathrm{\varphi }\in D$ , there is at least one algorithm $A\in P$ that performs fast on ϕ. Likewise, every algorithm in the portfolio performs fast on at least one formula from the dataset.

Fixed-Distance Selection. We call the following simple meta-algorithm the fixed-distance selector and denote it by S. The algorithm uses a dataset D and the corresponding portfolio P. Let ψ be a formula and let d be a non-negative integer. Taking ψ and d as input, the selector S either outputs an algorithm $A\in P$ or returns “can’t select”:

(1)

Find a formula $\mathrm{\varphi }\in D$ such that $\mathrm{\delta }(\mathrm{\varphi },\mathrm{\psi })⩽d$ and $\mathrm{\delta }(\mathrm{\varphi },\mathrm{\psi })$ is the minimum over all formulas $\mathrm{\varphi }\in D$ . If there is no such formula ϕ, return “can’t select”.

(2)

Select any algorithm A from $E_{\mathrm{\varphi }}$ and return it.

We do not specify how to find the formulas of D closest to ψ and how to choose one of them. The straightforward way of finding ϕ is exhaustive search: for $r=0,1,\dots ,d$ , enumerate all formulas $\mathrm{\varphi }\in D$ and verify whether $\mathrm{\delta }(\mathrm{\varphi },\mathrm{\psi })=r$ (the distance verification problem). It follows from Proposition 6 that each verification can be done using a polynomial-time oracle algorithm with an oracle for graph isomorphism. Thus, this exhaustive search requires at most $(d\mathbf{+}1)N$ runs of the oracle algorithm where N is the cardinality of the dataset.

What is the role of the input number d, should it be small or large? Proposition 11 gives an upper bound on the running time of the selected algorithm A on ψ. This bound depends on d: the smaller d is, the faster A is. On the other hand, assuming that N is fixed, if d is too small, this increases the chance that S returns “can’t select”. Thus, a good tradeoff for choosing d is needed.

Algorithms Matching with Parameters. An efficient performance of an algorithm A on a given class of formulas is typically due to the fact that A makes use of some “hidden structure” of formulas of this class. Different algorithms exploit different hidden structures and, thereby, they are successful on different classes of formulas. Hidden structures can be utilized explicitly or implicitly. For example, the fixed-parameter tractable algorithms mentioned in Section 5 make explicit use of certain properties of the incidence graph: the existence of a tree decomposition with a small treewidth and a small maximum deficiency. The CDCL $\mathrm{SAT}$ solvers in [2,13] can be viewed as examples of implicit use of community structures.

A hidden structure is often characterized by a parameter π such that the value $\mathrm{\pi }(\mathrm{\psi })$ determines how fast an algorithm A runs on ψ: the smaller $\mathrm{\pi }(\mathrm{\psi })$ is, the faster A on ψ is. For the most of such parameters, the running time of A on ψ is exponential in $\mathrm{\pi }(\mathrm{\psi })$ and polynomial in the size of ψ [6,15]. We say that A matches with π if there exist a number b and a polynomial q such that for every formula ψ, the running time of A on ψ is at most $b^{\mathrm{\pi }(\mathrm{\psi })}\mathbf{\cdot }q(l_{\mathrm{\psi }})$ where $l_{\mathrm{\psi }}$ is the size of ψ.

Note two differences between an algorithm A matching with a parameter π and a fixed-parameter algorithm. First, the input to A is a formula, while the input to a fixed-parameter algorithm is a formula along with a value of the parameter. Second, the upper bound for A has the exponential factor $b^{\mathrm{\pi }(\mathrm{\psi })}$ instead of an arbitrary function $f(\mathrm{\pi }(\mathrm{\psi }))$ as in the case of a fixed-parameter algorithm.

Conditions on Datasets and Portfolios. Let D be a dataset and P be the corresponding portfolio. Let a, b, and c be numbers and let q be a polynomial. We say that the tuple $(a,b,c,q)$ is a bound for D and P if for every formula $\mathrm{\varphi }\in D$ and every algorithm $A\in E_{\mathrm{\varphi }}$ , there exists a parameter π such that the following three conditions are met:

• Condition 1. $\mathrm{\pi }(\mathrm{\varphi })⩽a$ .

• Condition 2. The algorithm A matches with π and the corresponding base and polynomial are bounded from above by b and q respectively: for every formula ψ, the running time of A on ψ does not exceed $b^{\mathrm{\pi }(\mathrm{\psi })}\mathbf{\cdot }q(l_{\mathrm{\psi }})$ where $l_{\mathrm{\psi }}$ is the size of ψ.

• Condition 3. The parameter π is a parameter of constant variation and the corresponding bound on the change is less than or equal to c.

Proposition 11.

Let D be a dataset and P be the corresponding portfolio used by the fixed-distance selector S described above. Suppose that numbers a, b, c, and a polynomial q are bounds for D and P. Given a formula ψ and an integer d as input, let $A\in P$ be the algorithm returned by S on this input. Then the running time of A on ψ is at most $b^{a\mathbf{+}cd}\mathbf{\cdot }q(l_{\mathrm{\psi }})$ where $l_{\mathrm{\psi }}$ is the size of ψ.

Proof: Let $\mathrm{\varphi }\in D$ be the formula chosen by S as a formula closest to the input formula ψ. By Conditions 2 and 3, there is a parameter π such that

π is a parameter of constant variation;

A runs on ψ in time at most $b^{\mathrm{\pi }(\mathrm{\psi })}\mathbf{\cdot }q(l_{\mathrm{\psi }})$ .

By Proposition 10 we have $\mathrm{\pi }(\mathrm{\psi })⩽\mathrm{\pi }(\mathrm{\varphi })\mathbf{+}c\mathbf{\cdot }\mathrm{\delta }(\mathrm{\varphi },\mathrm{\psi })$ . By Condition 1 we have $\mathrm{\pi }(\mathrm{\varphi })⩽a$ . Therefore, $\mathrm{\pi }(\mathrm{\psi })⩽a\mathbf{+}cd$ .  □

Thus, A performs efficiently on ψ: assuming that d in the bound is fixed, there exists a polynomial $p(l)=b^{a\mathbf{+}cd}\mathbf{\cdot }q(l)$ such that the running time of A on ψ does not exceed $p(l_{\mathrm{\psi }})$ .

7. Concluding Remarks: Possible Extensions

Isomorphism of Formulas. There are several equivalent definitions of the distance δ (Proposition 2) and all of them use isomorphism of formulas as the central notion. On the other hand, these definitions do not require exactly our notion of isomorphism: two formulas are isomorphic if one of them can be obtained from the other by renaming variables and flipping literals. For example, we could define ${\mathrm{\varphi }}_1\simeq {\mathrm{\varphi }}_2$ based on only renaming, or only flipping, or another equivalence relation on formulas. In fact, we could define the distance relative to any equivalence relation on formulas: if I is such an equivalence relation, then ${\mathrm{\delta }}^I$ is the corresponding distance function on formulas. This distance ${\mathrm{\delta }}^I$ could be of interest for $\mathrm{SAT}$ solving if, first, the satisfiability status is preserved under I and, second, the problem of I-equivalence testing is “easier” than the problem of satisfiability testing (like the graph isomorphism problem is supposedly easier than the satisfiability problem).

Extension to CSP Instances. The main definitions and results of this paper can be extended from formulas in CNF to instances of the constraint satisfaction problem (CSP instances). The adjustments are obvious: clauses are replaced with constraints and isomorphism of formulas is replaced with isomorphism of CSP instances.

There are several variants of isomorphism of CSP instances; we describe the most common one. Let V be a finite set of variables that take values from a finite domain D. A constraint of arity k is a pair $(\overrightarrow{x},R)$ , where $\overrightarrow{x}$ is a k-ary tuple of variables from V and R is a k-ary relation on D. A CSP instance is a triple $(V,D,C)$ where C is finite set of constraints over V and D. Two CSP instances $(V_1,D_1,C_1)$ and $(V_2,D_2,C_2)$ are isomorphic if there are bijections $f:V_1\to V_2$ and $g:D_1\to D_2$ such that the set $C_2$ of constraints is obtained from $C_1$ by replacing each variable $x\in V_1$ and each value $a\in D_1$ with their images $f(x)$ and $g(a)$ respectively.

Using this variant of isomorphism, the definitions and propositions of Section 3 are easily carried over from formulas in CNF to CSP instances. Thus, the distance between two CSP instances ${\Phi }_1$ and ${\Phi }_2$ is the minimum number of constraints that can be removed from ${\Phi }_1$ and ${\Phi }_2$ so that the remaining sub-instances are isomorphic to each other. Or, equivalently, this distance is the minimum number of constraints that can be added to ${\Phi }_1$ and ${\Phi }_2$ so that the resulting “super-instances” are isomorphic to each other. The definitions and propositions regarding parameters of constant variation, their characterization in terms of the distance, and fixed-distance selection are carried over to CSP instances as well.