Improving Model Counting by Leveraging Definability

1 Introduction

Propositional model counting (alias the #SAT problem) is the task consisting in computing the number of models of a given propositional formula ⌃. This problem and its direct generalization, weighted model counting, are central to many AI problems including probabilistic inference [Sang et al., 2005; Chavira and Darwiche, 2008; Apsel and Brafman, 2012; Choi et al., 2013] and forms of planning [Palacios et al., 2005; Domshlak and Hoffmann, 2006]. They have also many applications outside AI, like in SAT-based automatic test pattern generation, for evaluating the vulnerability to malicious fault attacks in hardware circuits (see e.g., [Feiten et al., 2012]). However, propositional model counting is computationally hard (a #P-complete problem), actually much harder in practice than the satisfiability issue (the SAT problem). Its significance explains why much effort has been spent for the last decade in developing new algorithms for model counting (either exact or approximate) which prove practical for larger and larger instances [Samer and Szeider, 2010; Bacchus et al., 2003; Gomes et al., 2009].

In this paper, we present a new preprocessing technique for improving exact model counting. Preprocessing techniques are nowadays acknowledged as computationally valuable for a number of automated reasoning tasks, especially SAT solving and QBF solving [Bacchus and Winter, 2004;

Subbarayan and Pradhan, 2004; Lynce and Marques-Silva, 2003; Een and Biere, 2005; Piette et al., 2008; Han and Somenzi, 2007; Heule et al., 2010; J¨arvisalo et al., 2012; Heule et al., 2011]. As such, they are now embodied in some state-of-the-art SAT solvers, like Glucose [Audemard and Simon, 2009] which takes advantage of the SatELite preprocessor [Een and Biere, 2005], Lingeling [Biere, 2014] which has an internal preprocessor, and Riss [Manthey, 2012b] which takes advantage of the Coprocessor preprocessor [Manthey, 2012a].

Our approach elaborates on [Lagniez and Marquis, 2014], which describes a number of preprocessing techniques that can be exploited for improving the model counting task, computationally speaking. Among them is gate detection and replacement. Basically, every variable y of the input formula ⌃ which turns out to be defined in ⌃ in terms of other variables X = ¶x1, ▷ ▷ ▷ , xk♦ can be replaced by its definition ΦX, while preserving the number of models of ⌃. Indeed, whenever a partial assignment over the variables of X is considered, either it is jointly inconsistent with ⌃ or every model of ⌃ which extends this partial assignment gives to y the same truth value. In [Lagniez and Marquis, 2014], literal equivalences, AND/OR gates and XOR gates are detected (either syntactically or using Boolean Constraint Propagation). The empirical results reported in [Lagniez and Marquis, 2014] about the preprocessor pmc equipped with the so-called #eq combination of preprocessings clearly show that huge computational benefits can be achieved through the detection and the replacement of gates. However, pmc remains limited due to the small number of families of gates which are targeted (literal, AND, XOR gates and their negations).

In order to fill the gap, our preprocessing technique to model counting aims at exploiting in a much more aggressive way the existence of gates within the input formula ⌃. The key idea of our approach is that one does not need to identify the gates themselves but it can be enough to determine that such gates exist. To be more precise, it proves sufficient to detect that some definability relations between variables hold, without needing to identify the corresponding definitions. This distinction is of tremendous importance since on the one hand, the search space for the possible definitions ΦX is very large (2 2 k elements up to logical equivalence, when X contains k variables), and on the other hand, in the general case, the size of any explicit definition ΦX of y in ⌃ is not polynomially bounded in ♣⌃♣ + ♣X♣ unless NP \ coNP ✓ P/poly (which is considered unlikely in complexity theory) [Lang and Marquis, 2008].

Thus, in the following, we describe a new preprocessor B + E which associates with a given CNF formula 1 ⌃ a CNF formula Φ which has the same number of models as ⌃, but is at least as simple as ⌃ w.r.t. the number of variables and the size. B + E consists of two parts: B which aims at determining a Bipartition hI, Oi of the variables of ⌃ such that every variable of O is defined in ⌃ in terms of the remaining variables (in I), and E which aims at Eliminating in ⌃ some variables of O. Our contribution mainly consists of the presentation of the algorithms B and E, a property establishing the correctness of our preprocessor, and some empirical results showing the computational improvements for model counting offered by B + E compared to pmc. The benchmarks used, the implementation (runtime code) of B + E, some detailed empirical results, and a full-proof version of the paper are available on line from www.cril.fr/KC/.

The rest of the paper is organized as follows. Section 2 gives some background on propositional definability. In Section 3 we introduce our preprocessor B + E and prove that it is correct. Section 4 presents results from our large scale experiments, showing B + E as a challenging preprocessor for model counting, especially when compared with pmc. Finally, Section 5 concludes the paper and lists some perspectives for further research.

2 On Definability

Let L be the (classical) propositional language defined inductively from a countable set P of propositional variables, the usual connectives (≻, _, ^, $, etc.) and including the Boolean constants > and ?. Formulae are interpreted in the classical way. ♣= denotes logical entailment and ⌘ logical equivalence. For any formula ⌃ from L, Var(⌃) is the set of variables from P occurring in ⌃, and k⌃k is the number of models of ⌃ over Var(⌃). A literal ` is a variable ` = x from P or a negated one ` = ≻x. When ` is a literal, var(`) denotes the variable upon which ` is built. A term is a conjunction of literals or >, and a clause is a disjunction of literals or ?. A CNF formula is a conjunction of clauses. Let X be any subset of P. A canonical term γX over X is a consistent term into which every variable from X appears (either as a positive literal or as a negative one, i.e., as a negated variable). 9X.⌃ denotes any formula from L equivalent to the forgetting of X in ⌃, i.e., the strongest logical consequence of ⌃ which is independent of variables from X.

Let us now recall the two (equivalent) forms under which the concept of definability in propositional logic can be encountered:

1 Requiring the input to be a CNF formula is not a major restriction since Tseitin transformation [Tseitin, 1968] can be used to turn any propositional circuit into a CNF formula which has the same number of models - indeed, the variables which are introduced are actually defined from the original ones and the transformation consists in adding gates to the input. Interestingly, the CNF format is the one considered by state-of-the-art model counters.

Definition 1 (implicit definability) Let ⌃ 2 L, X ✓ P and y 2 P. ⌃ implicitly defines y in terms of X if and only if for every canonical term γX over X, we have γX ^ ⌃ ♣= y or γX ^ ⌃ ♣= ≻y.

Definition 2 (explicit definability) Let ⌃ 2 L, X ✓ P and y 2 P. ⌃ explicitly defines y in terms of X if and only if there exists a formula ΦX 2 PROPX s.t. ⌃ ♣= ΦX $ y. In such a case, ΦX is called a definition (or gate) of y on X in ⌃, y is the output variable of the gate, and X are its input variables.

Example 1 Let ⌃ be the CNF formula consisting of the following clauses:

d and e are implicitly defined in ⌃ in terms of X = ¶a, b, c♦. For instance, the canonical term γX = a ^ b ^ ≻c is such that γX ^ ⌃ ♣= d ^ ≻e. On the other hand, γ 0X = ≻a ^ ≻b ^ ≻c is such that γ 0X ^⌃ is inconsistent. d and e are also explicitly defined in ⌃ in terms of X = ¶a, b, c♦ since ⌃ implies

What happens in this example is not fortuitous due to the following theorem from [Beth, 1953]:

Theorem 1 Let ⌃ 2 L, X ✓ P and y 2 P. ⌃ implicitly defines y in terms of X if and only if ⌃ explicitly defines y in terms of X.

Since implicit definability and explicit definability coincide, one can simply say that y is defined in terms of X in ⌃. An interesting consequence of this theorem is that it is not mandatory to point out a definition ΦX of y in terms of X in order to prove that such a definition exists. Indeed, it is enough to show that ⌃ implicitly defines y in terms of X to do the job, and this problem is "only" coNP-complete [Lang and Marquis, 2008]. To prove it, we can take advantage of the following result (Padoa's theorem [Padoa, 1903]), restricted to propositional logic and recalled in [Lang and Marquis, 2008]; this theorem gives an entailment-based characterization of (implicit) definability:

Theorem 2 For any ⌃ 2 L and any X ✓ P, let ⌃0X be the formula obtained by replacing in ⌃ in a uniform way every propositional symbol z from Var(⌃) ∩ X by a new propositional symbol z0 . Let y 2 P. If y 62 X, then ⌃ (implicitly) defines y in terms of X if and only if ⌃ ^ ⌃0X ^ y ^ ≻y0 is inconsistent. 2

3 ANew Preprocessor toModel Counting

Instead of detecting gates and replacing them in ⌃ in order to remove output variables, our preprocessing technique consists in detecting output variables, then in forgetting them in ⌃. To be more precise, the objective is first to find (if possible) a definability bipartition hI, Oi of ⌃ where I contains as few elements as possible.

2 Obviously enough, in the remaining case when y 2 X, ⌃ defines y in terms of X.

Definition 3 (definability bipartition) Let ⌃ 2 L. A definability bipartition of ⌃ is a pair hI,Oi such that I [ O = Var(⌃), I \ O = ;, and ⌃ defines every variable o 2 O in terms of I.

Then in a second step, variables from O are forgotten in ⌃ so as to simplify it. This leads to the preprocessing algorithm B + E (B(ipartition), then E(liminate)) given at Algorithm 1:

Algorithm 1: B + E

input : a CNF formula ⌃ output: a CNF formula Φ such that kΦk = k⌃k O B(⌃); 1 Φ E(O,⌃); 2 return Φ 3

Interestingly, both steps in this algorithm can be tuned in order to keep the preprocessing phase light from a computational standpoint. On the one hand, it is not necessary to determine a definability bipartition hI, Oi of ⌃ for which the cardinality of I is minimal (identifying a reasonable amount of output variables can prove sufficient). On the other hand, it is not necessary to forget (i.e., eliminate) in ⌃ every variable from O but focusing on a subset E ✓ O is enough. Formally, our approach is based on the following result, which establishes the correctness of B + E:

Proposition 1 Let ⌃ 2 L. Let hI, Oi be a definability bipartition of Var(⌃). Let E ✓ O. Then k⌃k = k9E.⌃k.

The ability to identify only a subset O of output variables in the bipartition generation phase, and to consider only a subset E of O in the elimination phase is valuable. In fact, computing a shortest base (i.e., a subset I of minimal cardinality such that every variable not in I is definable in ⌃ in terms of I) [Lang and Marquis, 2008] would be prohibitive; indeed, computing such a base using a branch-and-bound algorithm would require, in the worst case, exponentially many definability tests in the number of variables occurring in ⌃. Furthermore, while forgetting variables in ⌃ obviously leads to diminishing the number of variables occurring in it, it may also lead to an exponential increase of its size. Eliminating in ⌃ only a subset E of variables from those found in O renders it possible to focus on those variables for which the elimination step will not increase the size of ⌃ (`a la NiVER [Subbarayan and Pradhan, 2004]), or only by a negligible factor. More generally, the elimination of an output variable can be committed only if the size of ⌃ after the elimination step remains small enough, once some additional preprocessing has been achieved. Among the equivalence-preserving preprocessings of interest are occurrence simplification [Lynce and Marques-Silva, 2003] and vivification [Piette et al., 2008] (already considered in [Lagniez and Marquis, 2014]), which aim at shortening some clauses, and at removing some clauses (for vivification).

Example 2 (Example 1 cont'ed) No literal equivalences, AND/OR gates or XOR gates are logical consequences of ⌃. Nevertheless, since ⌃ implies

a definability bipartition of Var(⌃) is h¶a, b, c♦, ¶d, e♦i. Now, forgetting d and e in ⌃ leads to the generation of two nonvalid clauses a _ c and a _ b _ c so that 9¶d, e♦.⌃ can then be computed as the conjunction of:

which can be simplified further into (a_b)^(a_c). This CNF formula has only 5 models, hence this is also the case of ⌃.

Algorithm 2: B

input : a CNF formula ⌃ output: a set O of output variables, i.e., variables defined in ⌃ in terms of I = Var(⌃) ∩ O h⌃,Oi backbone(⌃); 1 V sort(Var(⌃)); 2 I ;; 3 foreach x 2 V do 4 if defined?(x, ⌃, I [ succ(x, V), max#C) then 5 O O[ ¶x♦; 6 else 7 I I [ ¶x♦; 8 return O 9

Algorithm 2 shows how a bipartition hI,Oi of Var(⌃) is computed by B in a greedy fashion. At line 1, backbone(⌃) computes the backbone of ⌃ (i.e., the set of all literals implied by ⌃), and initializes O with the corresponding variables (indeed, a literal ` belongs to the backbone of ⌃ precisely when var(`) is defined in ⌃ in terms of ;). Boolean Constraint Propagation is also done on ⌃ completed by its backbone (this typically leads to simplifying ⌃). While the variables of the backbone can be simplified away in ⌃ by fixing their values, they are nevertheless kept in O in order to ensure that the set O of variables returned by B is such that ¶I,O♦ is a bipartition of Var(⌃). At line 2, the remaining variables occurring in ⌃ are sorted by considering their number of occurrences from less to more frequent. At line 4, defined? takes advantage of Padoa's method (Theorem 2) for determining whether x is defined in ⌃ in terms of I [ succ(x, V), where succ(x,V) is the set of all variables of V which appear after x in V. defined? takes advantage of an anytime SAT solver solve based on CDCL architecture for achieving the (un)satisfiability test required by Padoa's method. In our implementation, the input of solve is the CNF formula ⌃^⌃0;^ Vz2Var(⌃) ((≻sz_≻z_z0 ) ^(≻sz_z_≻z0 )), completed by assumptions: for every z belonging to I [ succ(x, V), the unit clause sz associated with z is added as an assumption to the CNF formula (its effect is to make z equivalent to its copy z0 ); then, x and ≻x0 are also added as assumptions. Interestingly, clauses which are learnt at each call to solve are kept for the subsequent calls. defined? is parameterized by max#C which bounds the number of clauses which can be learnt. When no contradiction has been found before max#C is reached, defined? returns false (i.e., x is considered as not defined in ⌃ in terms of I [ succ(x, V), while this could be questioned had a larger bound be considered). Clearly, the number of output variables found by B is not guaranteed to be maximal, but this is on purpose for the sake of efficiency (observe that the number of calls to solve does not exceed the number of variables occurring in ⌃).

Algorithm 3: E

input : a CNF formula ⌃ and a set of output variables O ✓ Var(⌃) output : a CNF formula Φ such that Φ ⌘ 9E.⌃ for some E ✓ O Φ ⌃; 1 iterate true; P O; 2 while iterate do 3 E P; P ;; iterate false; 4 Φ vivificationSimpl(Φ, E); 5 while E6= ; do 6 x select(E,Φ); 7 E E ∩ ¶x♦; 8 Φ occurrenceSimpl(Φ, x); 9 if #(Φx) ⇥ #(Φ≻x) > max#Res then 10 P P [ ¶x♦ 11 else 12 R removeSub(Res(x,Φ),Φ); 13 if #((Φ ∩ Φx,≻x) [ R)  #(Φ) then 14 Φ (Φ ∩ Φx,≻x) [R; 15 iterate true; 16 else 17 P P [ ¶x♦ 18 return Φ 19

Algorithm 3 shows how variables from O are eliminated in ⌃ by E. P contains variables x from O which are candidates for elimination. P is initialized with the full set O (line 2). The main loop at line 3 is repeated while the elimination of at least one variable is effective (line 16). At line 4, the set E of variables that will be tentatively eliminated during the iteration is initialized with P, and P is reset to ;. At line 5, the clauses of Φ are successively vivified using a slight variant of the vivification algorithm vivificationSimpl reported in [Lagniez and Marquis, 2014]. Vivification [Piette et al., 2008] is a preprocessing technique which aims at reducing the input CNF formula, i.e., to remove some clauses in it and some literals in the other clauses while preserving equivalence, using Boolean Constraint Propagation. The additional parameter E is used to sort the literals within the clauses of ⌃ so that the literals over E are put first (i.e., one tries to eliminate occurrences of literals over E in priority). At line 6, one enters into the inner loop that operates while there are remaining variables in E. At line 7, a variable x is selected in E for being possibly eliminated by counting the number #(Φx) of clauses of Φ where x appears as a positive literal, and the number #(Φ≻x) of clauses of Φ where ≻x appears as a negative literal; x is retained if it minimizes #(Φx)⇥#(Φ≻x), which is a upper bound of the number of resolvents that the elimination of x in Φ may generate. At line 8, x is removed from E. Then, at line 9, one tries first to eliminate in Φ some occurrences of variable x using occurrenceSimpl. occurrenceSimpl is a restriction of the algorithm for occurrence simplification reported in [Lagniez and Marquis, 2014], where instead of considering the whole set of literals occurring in Φ, we just focus on those in ¶x, ≻x♦. At line 10, one recomputes #(Φx)⇥#(Φ≻x) and checks whether it exceeds or not a preset bound max#Res. If this is the case, then we possibly postpone the elimination of x in Φ at the next iteration by adding it to P (line 11). Otherwise, we compute the set Res(x,Φ) of all non-valid resolvents of clauses from Φ on x and we remove from it using removeSub every clause which is properly subsumed by a clause of Φ or another clause from Res(x, Φ); the resulting set of clauses is R (line 13). At line 14, we test whether the elimination of x in Φ, obtained by removing from Φ its subset Φx,≻x of the clauses into which variable x occurs (either as a positive literal or as a negative literal), and adding the resolvents from R, leads or not to increasing the number of clauses in Φ. If so, we possibly postpone the elimination of x in Φ at the next iteration by adding it to P (line 18). If not, the elimination of x in Φ is committed (line 15). Clearly, it can be the case that some variables of O are not eliminated by E, but again, this is on purpose for efficiency reasons.

4 Empirical Results

In our experiments, we have considered 703 CNF instances from the SAT LIBrary. 3 They are gathered into 8 data sets, as follows: BN (Bayesian networks) (192), BMC (Bounded Model Checking) (18), Circuit (41), Configuration (35), Handmade (58), Planning (248), Random (104), Qif (7) (Quantitative Information Flow analysis - security). Our experiments have been conducted on Intel Xeon E5-2643 (3.30 GHz) processors with 32 GiB RAM on Linux CentOS. A time-out of 1h and a memory-out of 7.6 GiB has been considered for each instance. We set max#Res to 500.

As a matter of comparison, we have considered the pmc preprocessor for model counting, described in [Lagniez and Marquis, 2014] and available from www.cril.fr/KC/. To be more precise, we considered pmc equipped with the #eq combination of preprocessings, which combines backbone simplification, occurrence elimination, vivification and gates detection and replacement. pmc equipped with #eq proved empirically as a very efficient preprocessor for model counting [Lagniez and Marquis, 2014].

We evaluated the impact of B + E (for several values of max#C) by coupling it with exact model counters. We considered the search-based model counters Cachet 4 [Sang et al., 2004] and SharpSAT 5 [Thurley, 2006], run with their default settings. Though compilation-based approaches do much more than model counting (since they compute equivalent, compiled representations of the input CNF formula ⌃ and not only the number of models of ⌃), some of them appear as competitive for the model counting purpose. Thus, we also took advantage of the C2D compiler 6 [Darwiche, 2001; 2004] for achieving the downstream model counting task. C2D generates a Decision-DNNF representation ⌃⇤ of ⌃. The size of ⌃⇤ is exponential in the size of ⌃ in the worst case, but the number of models of ⌃ conditioned by any consistent term γ can be computed efficiently from ⌃⇤ in every case. And when γ is >, one gets the number of models of ⌃. C2D has been invoked with the following options -count -in memory -smooth all, which are suited when C2D is used as a model counter.

3 www.cs.ubc.ca/⇠hoos/SATLIB/index-ubc.html

4 www.cs.rochester.edu/⇠kautz/Cachet/

5 sites.google.com/site/marcthurley/sharpsat

By the way, it is worth noting that B + E cannot be considered upstream to compilation-based approaches to model counting, while preserving the possibility of counting efficiently the number of models of the input conditioned by any consistent term. Indeed, when B + E(⌃) is not equivalent to ⌃, the Decision-DNNF representation (B + E(⌃))⇤ computed by C2D is not equivalent to ⌃⇤ . Therefore, the possibility of efficient model counting after any conditioning is lost, but general conditioning must be downsized to a restricted form of conditioning where terms γ built up from I are allowed, but no other terms. Interestingly, such a restricted form of conditioning can prove enough in some scenarios. Especially, when the set of variables of ⌃ can be partitioned into a set of controllable variables (those which may require to be conditioned) and a remaining set of uncontrollable variables, one may take advantage of a slight variant of B + E ensuring that every controllable variable is put into I in order to simplify the input CNF formula ⌃ before compiling it.

The next table makes precise the number of instances (over 703) solved within 1h by each of the model counters Cachet, SharpSAT, and C2D (first column), when no preprocessing has been applied (second column), pmc (equipped with #eq) has been applied first (third column), and finally B + E(⌃) for several values of max#C has been applied first (the remaining columns). The preprocessing time is taken into account in the computations (it is part of the 1h CPU time allocated per instance).

The results reported in this table show the benefits which can be achieved by applying B + E before using a model counter. In particular, B + E leads to better performances than pmc. Since the best performances of B + E are achieved for max#C = 1, we focus on this parameter assignment in the following.

The cactus plot given in the next figure illustrates the performances of Cachet, SharpSAT, and C2D, possibly empowered by pmc or by B + E. For each value t on the y-axis (a model counting time, in seconds) and each dot of a curve for which this value is reached on the y-axis, the corresponding value on the x-axis makes precise how many instances have been solved by the approach associated with the curve within a time limit of t (which includes the preprocessing time, when In order to determine how much applying B + E leads to reduction of the input CNF formula ⌃ compared to pmc, we considered two measures for assessing the reduction of ⌃: #var(⌃), the number of variables of ⌃, and #lit(⌃), the number of literals occurring in ⌃ (i.e., the size of ⌃). Empirically, the results are presented on the two scatter plots (a) and (b) where each point corresponds to an instance ⌃, its x-coordinate corresponds to the value of the measure (#var (a) or #lit (b)) on pmc(⌃) equipped with the #eq combination of preprocessings, while its y-coordinate corresponds to the value of the same measure on B + E(⌃) (with max#Conflicts = 1). The scales used for both coordinates are logarithmic ones. Clearly enough, B + E often leads to much larger reductions than pmc for both measures. The benefits appear as very significant for instances from the Planning family.

6 reasoning.cs.ucla.edu/c2d/

Finally, we have evaluated how much B + E leads to reduction of the overall model counting time compared to pmc. The results are presented on the two scatter plots (with logarithmic scales) (c) and (d), for the two model counters Cachet and C2D (which appeared as the best counters in our experiments) considered downstream. Each point corresponds to an instance ⌃, its x-coordinate corresponds to the time (in seconds) required to compute k⌃k by computing pmc(⌃) first, then calling the model counter on the resulting CNF formula, while its y-coordinate corresponds to the time required to compute k⌃k by computing B + E(⌃) (with max#Conflicts= 1) first, then calling the model counter on the resulting CNF formula. Again, whatever the downstream model counter, B + E appears often as a more efficient preprocessor than pmc. The rightmost parts of the two scatter plots cohere with the results reported in the previous table, showing a number of instances which can be solved by any of the model counters when B + E has been applied first, while they cannot be solved within the time limit of 1h when pmc is used instead. Finally, note that considering only the preprocessing times (and not the overall time needed to count the number of models of the input) for evaluating the preprocessor would be misleading: for some instances, the preprocessing times can be (relatively) long (details are available from www.cril.fr/KC/), just because the preprocessor does almost all the job (it may happen that the simplification of the instance is so important that the downstreammodel counter has almost nothing to do afterwards).

5 Conclusion

We have defined a new preprocessing technique B + E which associates with a given CNF formula ⌃ a CNF formula B + E(⌃) which has the same number of models as ⌃, but is often simpler w.r.t. the number of variables and the size. B + E is based on standard theorems in classical logic by Beth and Padoa. Remarkably enough, while those results are quite old, they prove useful for defining a very effective preprocessing technique to model counting. Thus, experiments have shown that for many instances ⌃, the overall computation time needed to calculate kB + E(⌃)k using state-of-the art exact model counters is often much lower than the time needed to compute k⌃k with the same counters.

This work opens a number of perspectives for further re-

search. Considering other heuristics in B for determining a bipartition of the variables and determining how to tune the constants max#C and max#Res depending on the instance at hand will be studied in the future. Other perspectives concern the notion of projected model counting, as considered in [Aziz et al., 2015]. The purpose is to compute k9E.⌃k given a set E of variables and a formula ⌃. Instead of taking advantage of B + E followed by any model counter to compute k⌃k, we could instead use B followed by any projected model counter (where the projection is onto I). The other way around, we could also exploit E on E and ⌃ as a preprocessor for projected model counters. It would be interesting to implement both approaches and to determine whether they are helpful in practice.

Acknowledgments

We would like to thank the anonymous reviewers for their attentive reading, useful comments and advices.