Satisfiability Modulo Theories (SMT) refers to the problem of deciding the satisfiability of a formula with respect to certain background first-order theories. In this article, we focus on Satisfiablity Modulo Integer Arithmetic, which is referred to as SMT(IA), including both linear and non-linear integer arithmetic theories. Dominant approaches to SMT rely on calling a CDCL-based SAT solver, either in a lazy or eager flavour. Local search, a competitive approach to solving combinatorial problems including SAT, however, has not been well studied for SMT. We develop the first local-search algorithm for SMT(IA) by directly operating on variables, breaking through the traditional framework. We propose a local-search framework by considering the distinctions between Boolean and integer variables. Moreover, we design a novel operator and scoring functions tailored for integer arithmetic, as well as a two-level operation selection heuristic. Putting these together, we develop a local search SMT(IA) solver called LocalSMT. Experiments are carried out to evaluate LocalSMT on benchmark sets from SMT-LIB. The results show that LocalSMT is competitive and complementary with state-of-the-art SMT solvers, and performs particularly well on those formulae with only integer variables. A simple sequential portfolio with Z3 improves the state-of-the-art on satisfiable benchmark sets from SMT-LIB.
1 Introduction
Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order logic formula with respect to certain background theories. Inspired by the great success of propositional satisfiability (SAT) solving, SMT attempts to generalize the advances of satisfiability solvers from propositional logic to fragments of first-order logic. Typical theories supported by SMT include the theories of integers, real numbers, lists, arrays, and bit-vectors. The field of SMT has seen significant progress in the past two decades. SMT solvers have become important formal verification engines, with applications in various domains.
In this article, we focus on the theory of Integer Arithmetic (IA), consisting of arithmetic atomic formulae in the form of polynomial equalities or inequalities over integer variables. Integer Arithmetic can be divided into two categories, namely linearinteger arithmetic (LIA) and non-linear integer arithmetic (NIA), based on whether the arithmetic formulae purely consist of linear inequalities or not. The SMT problem with the background theory of LIA and NIA is to determine the satisfiability of the Boolean combination of respective arithmetic atomic formulae and propositional variables, and referred to as SMT(LIA) and SMT(NIA). Generally, the SMT problem of Integer Arithmetic is collectively referred to as SMT(IA).
SMT(IA) is important in software verification and automated reasoning, since most programs use integer variables and perform arithmetic operations on them [53]. Specifically, SMT(LIA) has various applications in automated termination analysis [24], sequential equivalence checking [51], and state reachability checking under weak memory models [34]. A popular fragment of LIA, namely Integer Difference Logic (IDL), has found applications in problems with timing-related constraints [26], such as hardware models with ordered data structures [33], stable models computing [41], and job shop scheduling [62]. SMT(NIA) has pervasive application in areas ranging from analysis, verification, and synthesis of software and hybrid systems [25, 60, 63, 64] to game theory [6].
1.1 Related Works
Much effort has been devoted to solving SMT on integer arithmetic. However, the approaches vary according to the corresponding theories. Techniques for solving SMT on linear integer arithmetic (LIA and IDL) can be divided into lazy and eager approaches. In contrast to SMT(LIA) and SMT(IDL), deciding SMT(NIA) is much more challenging, since the celebrated result of Matiyasevich [27] resolved Hilbert’s 10th problem in the negative by showing that satisfiability in the nonlinear case is undecidable. Thus the mainstream approaches for solving SMT on NIA are mainly incomplete.
The most popular approach for SMT(LIA) is the lazy approach [5, 65], also known as DPLL(T) [59], which is a central development of SMT. Many DPLL(T) solvers have been developed for SMT(LIA) [12, 30, 44]. In this approach, the formula is abstracted into a Boolean formula by replacing arithmetic atomic formulae with fresh Boolean variables. A SAT solver is used to reason about the Boolean structure and solve the Boolean formula, while a theory solver receives assignments from the SAT solver and solve the conjunctions of atomic subformulae, including consistency checking of the assignments and theory-based deduction.
The effort in the lazy approach is mainly devoted to producing more effective theory solvers. Simplex-based linear arithmetic solvers that can be integrated efficiently in the DPLL(T) framework were studied [30]. A simplex-based decision procedure that minimizes the sum of infeasibilities of constraints was proposed [45]. A theory solver made use of layering and several heuristics to achieve good performance [36]. A theory solver called SPASS-IQ was designed to efficiently handle unbounded problems [11, 13]. According to recent SMT Competitions,1 almost all state-of-the-art SMT(LIA) (including SMT(IDL)) solvers are based on the lazy approach, including MathSAT5 [23], CVC5 [4], Yices2 [29], Z3 [54], SMTInterpol [22], and SPASS-SATT [12].
The other approach for linear integer arithmetic is the eager approach, where the formula is reduced to an equi-satisfiable Boolean formula and then solved by a SAT solver. This approach works well for SMT(IDL). Typically, all intrinsic dependencies between integer variables are computed and encoded as Boolean constraints. Encoding to a Boolean formula is done either by deriving adequate ranges for formula variables (a.k.a. small domain encoding) [14, 61, 69], or by deriving all possible transitivity constraints (a.k.a per-constraint encoding) [68]. A hybrid method combining the strengths of two encoding schemes showed robust performance [67].
The mainstream approaches for SMT(NIA) are as follows. Most of the state-of-the-art SMT solvers supporting SMT(NIA) rely on the eager approach (bit-blasting) described in [32], where the problem is encoded to a SAT problem, by bounding the integer variables to a limited range. An approach relying on branch-and-bound has been explored in the context of CAD and VTS [46]. A novel method based on the MCSat (model-construction satisfiability) approach [43, 55] to SMT is proposed in [42], which reasons directly in the integers in a conflict-directed manner. An incomplete approach is proposed to solve SMT(NIA) by reducing it to SMT(LIA) [10]. Specifically, non-linear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. Moreover, the approach is further improved in [9] by deciding which domains to enlarge in each iteration, guided by analyzing solutions to optimization problems.
Local search is an incomplete method that plays an important role in many combinatorial problems [39]. Local search algorithms move from solution to solution in the space of candidate solutions by applying local changes. It has been successfully applied to the Boolean Satisfiability (SAT) problem [3, 7, 18, 20, 50] and is competitive with CDCL solvers on certain types of instances. However, very limited effort has been devoted to the local search for SMT. The idea of integrating local search solvers with theory solvers has been explored before, where a local search SAT solver WalkSAT is used to solve the Boolean skeleton of the SMT formula [37].
There are two main local-search approaches for solving SMT on the theory of bit vector (BV) by operating on the theory level. First, a local-search algorithm was proposed in [31]; it performs modifications to the assignment of the inputs that can be summarized as bit-level, including bit flips, inverting assignments, incrementing and decrementing the value by 1. It is guided by a scoring function and requires brute-force randomization and restart to avoid getting stuck in local minimums, which are successful techniques employed in local-search SAT solvers lifted to the SMT level.
In contrast, a precise propagation-based local search approach was presented in [57, 58], which is probabilistically approximately complete, indicating that it is guaranteed to find a solution theoretically. The approach is based on propagating target values from the outputs to the input, and does not require brute-force randomization or restarts. It lifts the concept of ATPG [47] to the word-level. The propagation-based local search approach is generalized in [56] with respect to constant bits to ternary values. The procedure is further extended to handle more bit-vector operators, and heuristics are introduced for more precise inverse value computation via bound tightening for inequality constraints.
We are not aware of any work on local search solvers for SMT on integer arithmetic theories.
1.2 Contributions
This work, for the first time, develops a local-search solver for SMT on the theory of quantifier-free Integer Arithmetic, denoted as SMT(IA), which directly operates on both Boolean and integer variables, breaking through the traditional approaches. The algorithm is a combination of several ideas, which are listed as follows:
(1)
We propose a local search framework, which switches between two modes, namely Boolean mode and Integer mode. Each mode consists of consecutive operations of the same type (either Boolean or integer), while keeping the assignments of variables of the other type fixed. In this way, the algorithm switches between solving subformulas consisting of only one type (either Boolean or Integer) of variables.
(2)
We propose a literal-level operator named critical move dedicated for Integer mode, which takes into account the literal-level information. Specifically, given a falsified literal and an integer variable in it, a critical move modifies the variable to the threshold value making the literal true.
(3)
A two-level heuristic is proposed to pick a critical move operation. We introduce a special type of decreasing (meaning the operation would decrease the value of a cost function) critical move operations based on the conflict driven principle, and give a priority to such operations.
(4)
A fine-grained scoring function named distance score is proposed to measure the decrement on the distance of falsified clauses to satisfaction by taking an operation. This is determined based on the cost function called the distance to truth of literals, which measures the distance of a falsified literal to becoming true.
By putting these together, we develop a local search solver for SMT(IA) called LocalSMT. Experiments are conducted to evaluate LocalSMT on 3 benchmark sets, including QF_LIA, QF_IDL and QF_NIA benchmark sets from SMT-LIB (excluding unsatisfiable insances).2 We compare our solver with state-of-the-art SMT solvers including Z3, CVC5, Yices and MathSAT5. Moreover, we also compare LocalSMT with 5 variants of the incomplete solver dedicated for SMT(NIA) in [9]. Experimental results show that LocalSMT is competitive and complementary with state-of-the-art SMT solvers. Particularly, LocalSMT is good at solving instances without Boolean variables, noting that a large portion in SMT-LIB (78.4% for LIA, 52.1% for IDL, and 88.7% for NIA) belong to this type. A simple sequential portfolio with Z3 improves the state-of-the-art on satisfiable benchmarks from SMT-LIB.
This article is the extended version of the conference article of CAV’22 [17], where a Local Search solver aimed at SMT(LIA) was proposed. The new contributions of this article include extending the local search algorithm to SMT(IA), being capable of solving SMT(NIA), and conducting more experiments on SMT-LIB to evaluate the performance of LocalSMT.
1.3 Article Organization
Some preliminary knowledge is introduced in Section 2. In Section 3, we propose a local search framework for SMT(IA). In Sections 4 and 5, we describe the two main ideas in the local search process, including the critical move operator and fine-grained scoring function, as well as a two-level heuristic for picking an operation which is a candidate variable/assignment pair. We describe the LocalSMT algorithm in Section 6. Experimental results and further analysis are presented in Section 7. Finally, we give some concluding remarks in Section 8.
2 Preliminary
A \(monomial\) is an expression of the form \(x_1^{p_1}...x_m^{p_m}\) where \(m\gt 0\), \(x_i\) are variables, \(p_i\gt 0\) for all \(i\in \lbrace 1...m\rbrace\), and \(x_i\not=x_j\) for all \(i,j\in \lbrace 1...m\rbrace ,i\not=j\). A monomial is linear if \(m=1\) and \(p_1=1\).
A \(polynomial\) is a linear combination of monomials, that is, an arithmetic expression of the form \(\sum _{i} a_i m_i\) where \(a_i\) are coefficients and \(m_i\) are monomials. A polynomial with only linear monomials, which can be written as \(\sum _i a_ix_i\), is \(linear\), and otherwise it is \(non-linear\). A special case of non-linear polynomials is a \(multilinear\) polynomial, where no variable occurs to a power of 2 or higher, meaning that each monomial is in the form of \(x_1...x_m\).
Definition 2.1.
Integer Arithmetic (IA): Let \(P=\lbrace p_1,p_2,...p_n\rbrace\) be a set of propositional (Boolean) variables and \(X=\lbrace x_1,x_2...x_m\rbrace\) be a set of integer-valued variables. Note that we refer to 0-arity function symbols as variables. The integer arithmetic formulae are inductively defined.
(1)
\(p\in P\) is a propositional atomic IA formula.
(2)
A polynomial inequality or equality (\(\sum _{i} a_i m_i\bowtie k\)) is an arithmetic atomic IA formula, where \(\bowtie \;\in \lbrace =,\le \rbrace\), \(m_i\) are monomials consisting of integer-valued variables, \(k\) and \(a_i\) are constant coefficients (rationals or integers).
(3)
If \(\psi\) and \(\varphi\) are IA formulae, so are \(\psi \vee \varphi\), \(\psi \wedge \varphi\) and \(\lnot \varphi\).
In the above definition, we note that with ‘\(\le\)’ and ‘\(=\)’, other inequalities can also be expressed. Specifically, we can express \(\sum _{i} a_i m_i\lt k\) as \(\sum _{i} a_i m_i\le k-1\), \(\sum _{i} a_i m_i\gt k\) as \(\lnot (\sum _{i} (a_i m_i)\le k)\), \(\sum _{i} a_i m_i\ge k\) as \(\sum _{i} (-a_i m_i)\le (-k)\) and \((\sum _{i} a_i m_i)\not=k\) as \((\sum _{i} a_i m_i\le (k-1)\vee \lnot (\sum _{i} (a_i m_i)\le k)\).
The arithmetic atomic formulae in Linear integer arithmetic (LIA) consist purely of linear polynomials, which can be written as \(\sum _i a_i x_i\bowtie k\), while those in more general non-linear integer arithmetic (NIA) are composed of polynomials. A popular fragment of linear integer arithmetic is called Integer Difference Logic (IDL), where the arithmetic atomic formulae are in the form of \(x_i-x_j\bowtie k\), where \(\bowtie \in \lbrace =,\le \rbrace\), \(x_i, x_j\in X\) and \(k\) is constant.
Example 2.2.
Let \(X=\lbrace x_1,x_2,x_3,x_4,x_5\rbrace\) and \(P=\lbrace p_1,p_2\rbrace\) denote the sets of integer-valued and propositional variables respectively. A typical SMT(LIA) formula \(F_{LIA}\) and SMT(NIA) formula \(F_{NIA}\) are shown as follows:
A literal is an atomic formula, or the negation of an atomic formula. A \(clause\) is the disjunction of a set of literals, and a formula in \(conjunctive\;normal\;form\) (CNF) is the conjunction of a set of clauses. For an SMT(IA) formula \(F\), an assignment \(\alpha\) is a mapping \(X\rightarrow Z\) and \(P\rightarrow \lbrace\)false,true\(\rbrace\), and \(\alpha (x)\) denotes the value of a variable \(x\) under \(\alpha\). A complete assignment is a mapping which assigns to each variable a value. A literal is a true literal if it evaluates to true under the given assignment, and otherwise it is a false literal. A clause is satisfied if it has at least one true literal, and falsified if all literals in the clause are false. A complete assignment is a solution to an SMT(IA) formula if and only if it satisfies all the clauses.
When applying local-search algorithms to solve a satisfiability problem, the search space consists of all complete assignments, each of which is a candidate solution. Typically, a local-search algorithm starts from a complete assignment, and iteratively modifies the assignment by changing the value of one variable to search for a satisfying assignment.
In local search, an operator defines how to modify the candidate solution. When an operator is instantiated with a variable to yield a value to assign to this variable, we obtain an operation. For example, a standard operator for SAT is flip, which modifies the current assignment by changing the value of a Boolean variable, and flip(\(x_1\)) is an operation, where \(x_1\) is a Boolean variable in the formula. Operators for integer variables typically have two parameters, namely the variable and the value to assign. We use \(op(x,v)\) to denote the operation assigning \(x\) to value \(v\).
Given a formula \(F\), the cost of an assignment \(\alpha\), denoted as \(cost(\alpha)\), is the number of falsified clauses under \(\alpha\). In this work, We adopt the dynamic local search (DLS) method [1, 40, 49], which is a popular local search method based on the idea of modifying the evaluation function in order to prevent the search from getting stuck in local minima. DLS typically employs weights modified during the search process. Thus, in this work, \(cost(\alpha)\) denotes the total weight of all falsified clauses under an assignment \(\alpha\). Given a formula and an assignment \(\alpha\), an operation \(op\) is said \(decreasing\) if \(cost(\alpha ^{\prime })\lt cost(\alpha)\), where \(\alpha ^{\prime }\) is the resulting assignment by applying \(op\) to \(\alpha\).
3 A Local Search Framework for SMT(IA)
In this section, we introduce a local search framework for SMT(IA), which switches between integer operations and Boolean operations.
Fig. 1.
Fig. 1. An SMT local search framework.
In the beginning, the algorithm generates a complete assignment \(\alpha\). Then, it iteratively modifies \(\alpha\) by performing operations on variables. The algorithm terminates once \(\alpha\) becomes a solution to the formula, and outputs “SATISFIABLE” as well as the solution. If the algorithm fails to find a solution within the pre-set time limit, it is cut off and outputs “UNKNOWN”.
As depicted in Figure 1, after the initialization, the algorithm works in two modes, namely Integer mode and Boolean mode. In each mode \(X\) (\(X\) is Integer or Boolean), an \(X\) operation is picked to modify \(\alpha\), where an \(X\) operation refers to an operation that works on a variable of data type \(X\). The two modes switches to each other when the number of non-improving steps (denoted as \(non\_improve\_steps\)) of the current mode reaches a threshold. The threshold is set to \(L\times P_b\) for the Boolean mode and \(L\times P_i\) for the Integer mode, where \(P_b\) and \(P_i\) denote the proportion of Boolean and integer literals to all literals in falsified clauses, and \(L\) is a parameter. Note that \(non\_improve\_steps\) is set to 0 whenever entering a mode, and then in each following step, it increases by one if \(cost(\alpha ^{\prime })\ge cost(\alpha)\) in the current step, where \(\alpha\) and \(\alpha ^{\prime }\) denotes the assignment before and after performing the operation.
The intuitions of the two mode framework are as follows. When all variables of one type (either Boolean or integer) are fixed, the formula is reduced to a subformula that contains only variables of the other type. Thus, by consecutively performing \(X\) (\(X\) can be Boolean or Integer) operations in a certain period, the algorithm focuses on dealing with a subformula consisting of only \(X\) variables. The switching threshold is set as \(L\times P_X\), as we consider that when \(X\) literals account for larger proportion of all literals in falsified clauses, more steps should be allocated for the corresponding mode.
Consider the situation when there is no Boolean literal in falsified clauses, indicating that \(P_ b=0\), but the algorithm fails to find an assignment in the following Integer mode. Note that the set of falsified clauses is altered after the Integer mode. If there exist Boolean literals in falsified clauses, indicating that \(P_b\gt 0\), the algorithm will switch to the Boolean mode and operates on Boolean variables. Otherwise, the \(non\_improve\_steps\) will be reset to 0, and the algorithm will enter the Integer Mode again. Thus, The algorithm will not get stuck.
Local search in one mode:
No matter the mode in which the algorithm works, it adopts a general procedure as described in Algorithm 1. It prefers to pick a decreasing operation (according to some heuristic) if any. If the algorithm fails to find any decreasing operation, it updates clause weights by increasing the weights of falsified clauses, and then picks an \(X\) operation from a random falsified clause containing \(X\) literals. Note that we can always pick a falsified clause with \(X\) literals (line 7). This is because when the algorithm works in \(X\) mode, since non_improve_steps\(\lt L\times P_X\), we have \(P_X\gt 0\), and so there exists at least one falsified clause with \(X\) literals.
As for clause weighting, our algorithm employs the probabilistic version of the PAWS scheme [20], which is evolved from the original PAWS scheme [70]. Note that the probabilistic PAWS is also adopted in previous local-search algorithm for SMT [31]. When the clause weighting scheme is activated, the clause weights are updated as follows. With probability \(1-sp\), the weight of each falsified clause is increased by one, and with probability \(sp\), for each satisfied clause whose weight is greater than 1, the weight is decreased by one.
4 The Critical Move Operator and A Two-level Heuristic
In this section, we introduce key techniques in the Integer mode of our method. We propose a novel operator called critical move. Moreover, a two-level heuristic is proposed for choosing a critical move in the Integer mode.
A key and basic component of a local search algorithm is the operator. For handling Boolean variables, our algorithm adopts the typical local search operator for SAT, namely flip, which modifies the value of a Boolean variable to the opposite of its current value (from True to False, or from False to True). For handling integer variables, we propose an operator called critical move which works on the literal level. First, we introduce the critical move dedicated for SMT(LIA), and then extend it to SMT(NIA).
4.1 Critical Move for SMT(LIA)
Different from the Boolean operator, an integer operator has two parameters – besides the variable to operate on, it also needs to consider the increment (may be positive or negative) on the value.
Let us first consider a simple operator, which motivates us to propose a literal-level operator. A simple integer operator is to modify the value of a variable \(a\) by a fixed increment \(inc\), that is, \(\alpha (a):=\alpha (a)\pm inc\). The parameter \(inc\) needs fine tuning. If \(inc\) is too small, it may take many iterations before making any falsified literal become true. If \(inc\) is too big, the algorithm may even become problematic that it can never make some literals true and thus essentially unable to solve some formulae.
Example 4.1.
Given a formula \(F: (b-a\ge 3)\wedge (b-a\le 5)\) and the current assignment is \(\alpha =\lbrace a=0, b=0\rbrace\). If \(inc=1\), it needs at least 3 operations to satisfy the formula. If \(inc=10\), then the formula cannot be satisfied using operations of this type, as the value of \(b-a\) would be always a multiple of 10.
In fact, in order to avoid the case that some literals can never become true (when the \(inc\) is too big), the only acceptable value of \(inc\) is 1. The main reason accounting for such a drawback is that the above operator ignores the literal-level information. We propose a literal-level operator for integer variables called critical move, which is defined below.
Definition 4.2.
The critical move operator \(cm\) has two parameters, a variable \(x\) and a literal \(\ell\) in the form of an arithmetic atomic formula containing \(x\) or its negation, and \(\ell\) is falsified under the current assignment. \(cm\) assigns \(x\) to the threshold value making literal \(\ell\) true.
We first present the critical move for LIA, while the case for NIA will be introduced in the next subsection. Given an arithmetic atomic LIA formulae \(\sum _{i}a_ix_i\bowtie k\), \(\bowtie \in \lbrace \le ,=\rbrace\), for each of the four basic forms of the falsified SMT(LIA) literal \(\ell\), we denote \(\Delta =\sum _{i}a_i\alpha (x_i)- k\). The operation \(cm(x,\ell)\) is described below:
—
\(\ell : \sum _{i}a_ix_i\le k\). There exists a cm operation \(cm(x_i,\ell)\) for each variable \(x_i\): if the coefficient \(a_i\gt 0\), then \(cm(x_i,\ell _1)\) decreases \(\alpha (x_i)\) by \(\lceil | \frac{\Delta }{a_i} | \rceil\);3 if \(a_i\lt 0\), then \(cm(x_i,\ell _1)\) increases \(\alpha (x_i)\) by \(\lceil | \frac{\Delta }{a_i} | \rceil\).
—
\(\ell : \lnot (\sum _{i}a_ix_i\le k)\), that is, \(\sum _{i}a_ix_i\gt k\). there exists a cm operation \(cm(x_i,\ell)\) for each variable \(x_i\): if the coefficient \(a_i\gt 0\), then \(cm(x_i,\ell _1)\) increases \(\alpha (x_i)\) by \(\lceil | \frac{1-\Delta }{a_i} | \rceil\); if \(a_i\lt 0\), then \(cm(x_i,\ell _1)\) decreases \(\alpha (x_i)\) by \(\lceil | \frac{1-\Delta }{a_i} | \rceil\).
—
\(\ell : \sum _{i}a_ix_i= k\). There exists an operation \(cm(x_i,\ell)\) for each variable \(x_i\) with coefficient \(a_i\mid \Delta\),4 which increases \(\alpha (x_i)\) by \(-\frac{\Delta }{a_i}\).
—
\(\ell : \lnot (\sum _{i}a_ix_i= k)\). There exist 2 cm operations for each variable \(x_i\), to increment or decrement \(x_i\) by 1.
Example 4.3.
Assume we are given two falsified literals \(l_1: (2b-a\le -3)\) and \(l_2: (5c-d+3a=5)\), and the current assignment is \(\alpha =\lbrace a=0,b=0,c=0,d=0\rbrace\). Then \(cm(a,l_1)\), \(cm(b,l_1)\), \(cm(c,l_2)\), and \(cm(d,l_2)\) refers to assigning \(a\) to 3, assigning \(b\) to \(-2\), assigning \(c\) to 1 and assigning \(d\) to \(-5\) respectively. Note that there does not exist \(cm(a,l_2)\), since \(-5\) is not divisible by 3.
An important property of the cm operator is that after the execution of a cm operation, the corresponding literal must be true. Therefore, by picking a falsified literal and performing a cm operation on it, we can make the literal become true.
Given the above definition of the critical move, an issue with this operator is that it may stall on equalities, when there is no such variable with coefficient \(a_i\mid \Delta\) in \(\ell\). To address this issue, in this situation, we additionally employ a simple strategy — we pick a random variable in that literal and to increment or decrement the value of the variable by 1, which can decrease \(| \Delta |\). For example, given an equality \(2a+3b=5\), where the assignment is \(\lbrace a=0,b=0\rbrace\), since there exists no variable with coefficient which divides \(\Delta =-5\), we pick a random variable such as \(a\), and increment \(a\) by 1 to decrease \(| \Delta |\).
The critical move operations are analogous to update operations in other linear arithmetic model searching procedures. For example, Simplex for DPLL(T) [28] also progresses through a sequence of candidate assignments by updating the assignment to a variable to satisfy its bound. The significant distinction of critical moves is only updating input variables and always updating by an integral amount, as we can see from Definition 2.
4.2 Critical Move for SMT(NIA)
We further extend the Definition 4.2 of Critical Move to SMT(NIA) literals. Note that variables in NIA can have a degree greater than 1 in a polynomial. Consider an equation with respect to the polynomial of a given literal; when all variables but one are fixed to a value, there are often multiple roots with respect to that variable (if its highest degree is greater than 1). This would lead to a set (instead of just one) of \(cm\) operations for such a variable w.r.t. the literal.
Given an arithmetic atomic formula \(f: \sum _i a_i m_i\bowtie k\), \(\bowtie \in \lbrace \le ,=\rbrace\), where each \(m_i\) is a monomial, consider the corresponding equation \(\sum _i a_i m_i-k=0\). For a variable \(x\) in \(f\), when all variables except \(x\) in the equation are substituted by its assignment, we then have an equation for \(x\), written as \(\sum _i a_i m_i(x)-k=0\). Let us introduce some notation before describing the critical move for NIA.
—
Suppose \(x\) has \(n\) different roots for \(\sum _i a_i m_i(x)-k=0\), we list them as \(r_1\lt r_2\lt \dots \lt r_n\).
—
Let \(s_j\in \lbrace +,-\rbrace\) denote the sign of \((\sum _i a_i m_i(x)-k)\) in the interval \((r_j,r_{j+1})\), \(j\in \lbrace 0,\ldots ,n\rbrace\). For the sake of convenience, we add \(r_0\) and \(r_{n+1}\) to denote \(-\infty\) and \(\infty\) respectively, although \(r_0\) and \(r_{n+1}\) are not roots.
Now, we are ready to describe the critical move for NIA. For each of the four basic forms of a falsified SMT(NIA) literal \(\ell\) and one of its variables \(x\), applying the critical move operator to \(x\) w.r.t. \(\ell\) leads to a set of operations, depending on the roots \(r_j\) and signs \(s_j\) of the corresponding polynomial. In order to distinguish from LIA, the operation set is denoted as \(cm_{NIA}(x,\ell)\). Recall that \(op(x,v)\) denotes an operation assigning \(x\) to value \(v\). Detailed description is as follows.
—
\(\ell : \sum _{i}a_im_i\le k\). We have a set of critical moves as below:
where \(S^-=\lbrace j\in \lbrace 0,\ldots ,n\rbrace | s_j=\) ‘\(-\)’\(\rbrace\), \(I_{min}[r_j,r_{j+1}]\) and \(I_{max}[r_j,r_{j+1}]\) refers to the smallest and biggest integer in the interval \([r_j,r_{j+1}]\), respectively. Note that \(r_0\) and \(r_{n+1}\) refers to \(-\infty\) and \(+\infty\), and thus we never include \(op(x,I_{min}[r_0,r1])\) or \(op(x,I_{min}[r_n,r_{n+1}])\) in the set.
—
\(\ell : \lnot (\sum _{i}a_im_i\le k)\), that is, \(\sum _{i}a_ix_i\gt k\). We have a set of critical moves as below:
where \(S^+=\lbrace j\in \lbrace 0,\ldots ,n\rbrace | s_j=\) ‘\(+\)’\(\rbrace\) and \(I_{min}(r_j,r_{j+1})\) and \(I_{max}(r_j,r_{j+1})\) refers to the smallest and biggest integer in the interval \((r_j,r_{j+1})\), respectively. Again, we never include \(op(x,I_{min}(r_0,r1))\) or \(op(x,I_{min}(r_n,r_{n+1}))\) in the set.
\(\ell : \lnot (\sum _{i}a_im_i= k)\). There exist 2 operations for each variable \(x\), to increment or decrement \(x\) by 1.
Example 4.4.
Assume we are given two falsified literals \(l_1: (-2bc^2+3ab+c\le -3)\) and \(l_2: (5a-d^2=5)\), and the current assignment is \(\alpha =\lbrace a=1,b=1,c=1,d=1\rbrace\). To calculate \(cm_{NIA}(c,l_1)\), the variables except \(c\) in the arithmetic NIA formula are substituted by its assignment, resulting in the equation corresponding to \(c\): \(-2c^2+c+6=0\). Then we need to figure out the roots of the equation, that is \(r_1=-1.5,r_2=2\), and signs of corresponding intervals. The interval corresponds to \(-2c^2+c+6\le 0\) is \((-\infty ,-1.5]\) and \([2,\infty)\), and thus \(cm_{NIA}(c,l_2)=\lbrace op(c,2),op(c,-2)\rbrace\). Similarly, \(cm_{NIA}(a,l_1)=\lbrace op(a,-1)\rbrace\), \(cm_{NIA}(b,l_1)=\lbrace op(b,-4)\rbrace\), and \(cm_{NIA}(d,l_2)=\lbrace op(d,0)\rbrace\). Note that \(cm_{NIA}(a,l_2)\) contains no operation, since there is no integer root for \(5a-6=0\).
Under circumstances where the non-linear arithmetic atomic formula is a multilinear polynomial, the critical move degenerates to the same as that in SMT(LIA). In other words, the calculation of \(cm\) operation in context of LIA is a special case of that in the context of NIA.
Note that calculating the integer solution of equations of higher degree can be time-consuming in practice, and thus in order to improve efficiency, when the variable \(x\) occurs to a power of 3 or higher in the falsified literal \(\ell\), the corresponding critical move \(cm(x,\ell)\) will not be considered.
4.3 A Two-level Heuristic
In this subsection, we propose a two-level heuristic for selecting a decreasing cm operation. We distinguish a special type of decreasing cm operations from others, and give a priority to such operations.
From the viewpoint of algorithm design, there is a major difference between cm and flip operations. A flip operation is decreasing only if the flipping variable appears in at least one falsified clause. For a decreasing critical move operation in a falsified literal \(\ell\), \(\ell\) does not necessarily appear in any falsified clause. This is because \(\ell\) has different variables, and changing one such variable will affect all other literals (not only \(\ell\)) containing the variable.
Example 4.5.
Given a formula \(F=c_1 \wedge c_2 = (a-b\le 0\vee b-e\le -2 \vee bd-a\le -3)\wedge (b-d\le -1)\), suppose the current assignment is \(\alpha =\lbrace a=1, b=1, d=1, e=1\rbrace\), then \(c_1\) is satisfied and \(c_2\) is falsified. The operation \(op1=cm(b, b-e\le -2)\) and \(op2=cm(b, b-d\le -1)\) refers to assigning \(b\) to \(-1\) and 0, respectively. The only operation in \(cm_{NIA}(b,bd-a\le -3)\), denoted as \(op3\), refers to assigning \(b\) to \(-2\). The literal of \(op1\) and \(op3\) does not appear in any falsified clause while the literal of \(op2\) appears in a falsified clause \(c_2\). All operations are decreasing, as either of them would make clause \(c_2\) become satisfied without breaking any satisfied clause.
In order to find a decreasing cm operation whenever one exists, we need to scan all cm operations on false literals. Let us use \(D\) to denote the candidate set of decreasing cm operations.
—
For LIA: \(D=\lbrace cm(x,\ell)| \ell\) is a false literal and \(x\) appears in \(\ell \rbrace\);
—
For NIA: \(D=\lbrace op| op\) belongs to some \(cm_{NIA}(x,\ell)\), where \(\ell\) is a false literal and \(x\) appears in \(\ell \rbrace\).
If \(D=\emptyset\), there is no decreasing cm operation. We propose to distinguish a special subset \(S\subseteq D\) from the rest of \(D\), which contains cm . For LIA, \(S=\lbrace cm(x,\ell)|\ell\) appears in at least one falsified clause and \(x\) appears in \(\ell \rbrace\). In the context of NIA, \(S=\lbrace op| op\) belongs to some \(cm_{NIA}(x,\ell)\), where \(\ell\) appears in at least one falsified clause and \(x\) appears in \(\ell \rbrace\). Note that any cm operation in \(S\) would make at least one falsified clause become satisfied. Based on this distinction, we propose a two-level selection heuristic as follows:
—
The heuristic prefers to search for a decreasing cm operation from \(S\).
—
If it fails to find any decreasing operation from \(S\), then it searches for a decreasing cm operation from \(D\setminus S\).
Besides improving the efficiency of picking a decreasing cm operation, there is an important intuition underlying this two-level heuristic. We prefer to pick a decreasing cm operation from \(S\), because such operations are conflict driven, as any \(cm\in S\) would force a falsified clause become satisfied. This idea can be seen as an IA version of focused local search for SAT, which has been the core idea of WalkSAT-family SAT solvers [3, 7, 66].
5 Scoring Functions
Most local search algorithms employ scoring functions to guide the search [19, 20, 21, 49]. We introduce two scoring functions, which are used to compare different operations and guide the local search algorithm to pick an operation to execute in each step.
A perhaps most commonly used scoring function for SAT, denoted as score, measures the change on the cost of the assignment by flipping a variable. This scoring function indeed can be used to evaluate all types of operations as it only concerns the clauses’ state (satisfied or falsified). We also employ score in our algorithm, for both flip and cm operations. Formally, the score of an operation is defined as
where \(\alpha ^{\prime }\) is obtained from \(\alpha\) by applying \(op\). Note that our algorithm employs a clause weighting scheme which associates a positive integer weight to each clause, and thus the \(cost\) of an assignment is the total weight of falsified clauses. An operation \(op\) is \(decreasing\) if and only if \(score(op)\gt 0\). Our algorithm prefers to choose the operation with greater \(score\) in the greedy mode, for both Boolean and integer operations.
For integer operations, we propose a more fine-grained scoring function, measuring the potential benefit about pushing a falsified literal towards the direction of becoming true. Firstly, we propose a property of literals to measure this merit.
Definition 5.1.
Given an assignment \(\alpha\), for an arithmetic literal \(\ell : \sum _{i}a_ix_i\le k\), its distance to truth is \(dtt(\ell ,\alpha)=max\lbrace \sum _{i}a_i\alpha (x_i)-k,0\rbrace\). For a Boolean literal \(\ell\) and an arithmetic literal \(\ell : \sum _{i}a_ix_i= k\), \(dtt(\ell ,\alpha)=0\) iff \(\ell\) is true under \(\alpha\) and \(dtt(\ell ,\alpha)=1\) otherwise.
Suppose the current assignment is \(\alpha\), for an arithmetic literal \(\ell : \sum _{i}a_ix_i\le k\), if \(\sum _{i}a_i\alpha (x_i)\gt k\), then the literal is falsified, and its \(dtt\) is defined to be \(\sum _{i}a_i\alpha (x_i)-k\). In this case, if we decrease the value of \(x_i\) with \(a_i\gt 0\), or increase the value of \(x_i\) with \(a_i\lt 0\), the \(dtt\) of \(\ell\) would decrease. When \(\sum _{i}a_i\alpha (x_i)\le k\), the literal \(\ell\) is true, and thus its \(dtt\) is defined to be 0.
The definition of \(dtt\) for arithmetic literals resembles the violation function for constraint satisfaction problems [38] and the violation operator in the simplex with sum of infeasibilities for SMT [45]. In this work, we extend it to the clause level to measure the distance to satisfaction of a clause in a fine-grained manner. Based on the concept of distance to truth of literals, we define a function to measure the distance to satisfaction of a clause.
Definition 5.2.
Given an assignment \(\alpha\), the distance to satisfaction of a clause \(c\) is \(dts(c,\alpha)=min_{\ell \in c}\lbrace dtt(\ell ,\alpha)\rbrace\).
According to the definition, the \(dts\) is 0 for satisfied clauses, since there is at least one satisfied literal with \(dtt=0\), while \(dts\) is positive for falsified clauses. It is desirable to lead the algorithm to decrease the \(dts\) of clauses. To this end, we propose a scoring function to measure the benefit of decreasing the sum of \(dts\) of all clauses. Additionally, the function takes into account the clause weights as the \(score\) function.
Definition 5.3.
Given an LIA formula \(F\), the distance score of an operation \(op\) is defined as
where \(\alpha\) and \(\alpha ^{\prime }\) denotes the assignment before and after performing \(op\).
For Boolean flip operations, \(dscore\) is equal to \(score\). For integer operations, however, compared to the \(score\) function which only concerns the state (satisfied or falsified) transformations of clauses, \(dscore\) is more fine-grained, as it considers the \(dts\) of clauses, which are different among falsified clauses.
Example 5.4.
Given a formula \(F=c_1\wedge c_3\wedge c_3=(a-b\le -1)\wedge (a-c\le -5\vee a-d\le -10)\wedge (b-c\le -5\vee b-d\le -10)\). Suppose \(w(c_1)=1, w(c_2)=2, w(c_3)=3\), and the current assignment is \(\alpha =\lbrace a=0,b=0,c=0,d=0\rbrace\), and thus all clauses are falsified. Consider two cm operations \(op1=cm(a,a-b\le -1)\) and \(op2=cm(b,a-b\le -1)\), which assign \(\alpha (a):=-1\) and \(\alpha (b):=1\) respectively, leading to \(\alpha ^{\prime }\) and \(\alpha ^{\prime \prime }\) respectively. Then \(score(op1)=score(op2)=1\), as they both make \(c_1\) satisfied. Also, \(dts(c_2,\alpha)-dts(c_2,\alpha ^{\prime })=1\), and \(dts(c_3,\alpha)-dts(c_3,\alpha ^{\prime \prime })=-1\), so \(dscore(op1)=(dts(c_1,\alpha)-dts(c_1,\alpha ^{\prime }))\cdot w(c_1)+(dts(c_2,\alpha)-dts(c_2,\alpha ^{\prime }))\cdot w(c_2)= 1\times 1+1\times 2=3\) and \(dscore(op2)=-2\) by similar calculation. Therefore, \(op1\) is a better operation.
Since the computation of \(dscore\) has considerable overhead, this function is only used when there is no decreasing operation. As the reader will see in the next section, when there is no decreasing operation, only a limited number of non-decreasing operations are tried, and thus it is affordable to calculate their \(dscore\).
Note that \(dscore\) is not extended to SMT(NIA), since arithmetic atomic formulas in SMT(NIA) may consist of variables with exponent greater than 1, whose modification would dramatically affect the value of polynomials, and thus may mislead the search process. Therefore, our solver does not use \(dscore\) in the context of SMT(NIA).
We end this section by noting that it is usually desirable to design dedicated scoring functions for different theories. Besides this work, another example is the scoring function based on a recursive function for SMT(BV) [31]. Some local search algorithms can even work without any scoring function, by using propagation techniques instead [56, 57].
6 A Local Search Algorithm for SMT(IA)
Based on the ideas in previous sections, we design a local search algorithm for SMT(IA), and implement a solver called LocalSMT, which can be used to solve SMT formulas on integer arithmetic theories, including SMT(LIA) and SMT(NIA). As described in Section 3, after the initialization, the local search works in either Boolean or Integer mode to iteratively modify \(\alpha\) until a given time limit is reached or \(\alpha\) satisfies the formula \(F\). This section is dedicated to the details of the initialization and the two modes of local search, as well as other optimization techniques.
Initialization: LocalSMT generates a complete assignment \(\alpha\), by assigning the variables one by one until all variables are assigned. All Boolean variables are assigned to True. As for an integer variable \(x_i\), if it has upper bound \(ub\) and lower bound \(lb\), that is, there exist unit clauses \(x_i\le ub\) and \(x_i\ge lb\), it is assigned to a random value in \([lb,ub]\). If \(x_i\) only has upper (lower) bound, \(x_i\) is assigned to \(ub(lb)\). Otherwise, if the variable is unbounded, it is assigned to 0.
Boolean Mode (Algorithm 2): If there exist decreasing flip operations, the algorithm selects such an operation with highest \(score\). If the algorithm fails to find any decreasing operation, it first updates clause weights according to the weighting scheme described in Section 3. Then, it picks a random falsified clause with Boolean literals and chooses a flip operation with greatest \(score\).
Integer Mode (Algorithm 3): If there exist decreasing cm operations, the algorithm chooses a cm operation using the two-level heuristic: it first traverses falsified clauses to find a decreasing cm operation with greatest \(score\) (line 3–4); if no such operation exists, it searches for a decreasing cm operation via BMS heuristic (line 5–6) [15]. Specifically, according to BMS heuristic, the algorithm samples \(t\)cm operations (\(t\) is a parameter) from the false literals in satisfied clauses, and selects the decreasing one with greatest \(score\). If the algorithm fails to find any decreasing operation, it first updates clause weights similarly to the Boolean mode. Then, in the context of SMT(LIA) (respectively SMT(NIA)) it picks a random falsified clause with Integer literals and chooses a cm operation with highest \(dscore\) (respectively \(score\)).
Restart Mechanism: The search is restarted when the number of falsified clauses has not decreased for \(MaxNoImprove\) iterations, where \(MaxNoImprove\) is a parameter. In previous local-search algorithms for SMT (in the context of BV), an exponential restart schema similar to the Luby schema for CDCL solvers [52] is adopted in [31], while some other local search algorithms for SMT(BV) do not incorporate any restart mechanism [56, 57].
Forbidding Strategies: Local search methods tend to be stuck in suboptimal regions. To address the cycle phenomenon (i.e., revisiting some search regions), we employ a popular forbidding strategy, called the tabu strategy [35]. After an operation is executed, the tabu strategy forbids the reverse operations in the following \(tt\) iterations, where \(tt\) is a parameter usually called tabu tenure. The tabu strategy can be directly applied in LocalSMT. (1) If a flip operation is performed to flip a Boolean variable, then the variable is forbidden to flip in the following \(tt\) iterations. (2) If a cm operation that increases (decreases, respectively) the value of an integer variable \(x\) is performed, then it is forbidden to decrease (increase, respectively) the value of \(x\) in the following \(tt\) iterations.
This might be the first time a forbidding strategy is applied in local-search algorithms for SMT.
Discussion of Completeness: Our algorithm is not complete in the sense of probabilistically approximately complete (PAC) based on the following reasons. First, the \(cm\) operation always assigns the variable to the threshold value to satisfy a literal, and thus it can miss the possible satisfying solution where variables are not necessarily on the threshold to satisfy a literal. Moreover, in the case of NIA, when the variable occurs to a power of 3 or higher in a falsified literal, the corresponding \(cm\) operation is not considered, and thus the search space cannot be thoroughly traversed.
7 Experiments
We carry out experiments to evaluate our solver LocalSMT on 3 benchmark sets from SMT-LIB, and compare it with state-of-the-art SMT solvers. We also compare our solver with incomplete solvers dedicated for SMT(NIA). Moreover, we combine LocalSMT with Z3 to obtain a sequential portfolio solver, which shows further improvement. Additionally, experiments are conducted to analyze the effectiveness of the proposed ideas.
7.1 Experiment Preliminaries
Implementation: LocalSMT is implemented in C++ and compiled by g++ with “-O3” option. There are 5 parameters in LocalSMT: \(L\) for switching phases, \(tt\) for the tabu scheme, \(MaxNoImprove\) for restart, \(t\) (the number of samples) for the BMS heuristic and \(sp\) (the smoothing probability) for the PAWS scheme. The parameters are tuned according to suggestions from the literature and our preliminary experiments on 20% sampled instances, and are set as follows: \(L=20\), \(t=45\), \(tt=3+rand(10)\), \(MaxNoImprove=500,000\) and \(sp=0.0003\) for all benchmarks.
Competitors: We compare LocalSMT with 4 state-of-the-art SMT solvers according to SMT-COMP 2021,5 namely MathSAT5 (version 5.6.8), CVC5 (version 1.0.2), Yices2 (version 2.6.4), and Z3 (version 4.8.17), which are the union of the top 4 solvers (excluding portfolio solvers) of QF_NIA, QF_LIA and QF_IDL tracks. In the context of SMT(NIA), we also compare LocalSMT with 5 variants of the incomplete solvers dedicated to SMT(NIA) in [9], namely bcl-maxsmt, bcl-ninc-cores, bcl-ninc, bcl-omt and bcl-cores. The binaries of all competitors are downloaded from their websites.
Benchmarks: Our experiments are carried out on 3 benchmark sets from SMT-LIB. As LocalSMT is an incomplete solver, UNSAT instances are excluded.
—
SMTLIB-LIA: This benchmark set consists of 8,512 unknown and satisfiable SMT(LIA) instances from SMT-LIB.6
—
SMTLIB-IDL: This benchmark set consists of 1,611 unknown and satisfiable SMT(IDL) instances from SMT-LIB.7
—
SMTLIB-NIA: This benchmark set consists of 18,419 unknown and satisfiable SMT(NIA) instances from SMT-LIB.8
Instances from SMTLIB-LIA, SMTLIB-IDL, and SMTLIB-NIA benchmark sets are divided into two categories depending on whether they contain Boolean variables. From the viewpoint of algorithm design, there is a major difference between the operations on Boolean and integer variables. We observe that instances containing only integer variables make up a large proportion, amount to 78.4%, 52.1%, and 88.7%, in these three benchmark sets.
Since names of recently uploaded benchmarks are too long, in order to save space, they are renamed by only using the type and uploaded year.
Experiment Setup: All experiments are carried out on a server with Intel Xeon Platinum 8,153 2.00 GHz and 2,048G RAM under the system CentOS 7.9.2009. Each solver is executed with a cutoff time of 1,200 seconds (as in the SMT-COMP) for each instance in SMT-LIB, as they contain sufficient instances. “#inst” denotes the number of instances in each family. We compare the number of instances where an algorithm finds a model (“#solved”), as well as the run time. The bold value in table emphasizes the solver with greatest “#solved”.
Our solver is uploaded as a part of a derived solver called Z3++,9 which won the Biggest Lead and Largest Contribution Gold Medal in Model-validation Track of SMT-COMP 2022.
We organize the results into two categories: instances Without Boolean variables, and instances With Boolean variables. LocalSMT outperforms its competitors on the Without Boolean category, solving 6,478 out of the 6,670 instances. We also present the run time comparisons between LocalSMT and each competitor on the Without Boolean category of SMTLIB-LIA benchmark set in Figure 2.
Fig. 2.
Fig. 2. Run time comparison on Without Boolean category of SMTLIB-LIA.
As for the With Boolean category, the performance of LocalSMT is overall worse than its competitors, but still comparable. A possible explanation is that as local search SAT solvers, LocalSMT is not good at exploiting the relations among Boolean variables. Nevertheless, LocalSMT has obvious advantage in “tropical-matrix” and “arctic-matrix” instances, which are industrial instances from automated program termination analysis [24]. LocalSMT can exclusively solve 18 and 27 instances on these two types, showing its complementary performance compared to CDCL(T) solvers.
Table 2.
Family
Type
#inst
MathSAT
CVC5
Yices2
Z3
LocalSMT
Without Boolean
Bouvier(2021)
100
4
42
38
56
41
DTP
32
32
32
32
32
32
job_shop
108
47
63
74
74
76
jobshop(2022)
119
26
28
48
44
75
n_queen
97
64
97
97
92
97
RVpredict(2022)
15
15
15
15
5
15
schedulingIDL
247
105
162
247
247
247
super_queen
91
59
90
91
91
91
toroidal_bench
32
11
10
12
12
13
total
841
363
539
654
653
687
With Boolean
asp
379
147
212
284
291
27
Averest
157
157
157
157
157
120
bcnscheduling
6
3
4
4
4
4
fuzzy-matrix
15
0
0
0
0
1
mathsat
16
16
16
16
16
11
parity
136
130
136
136
136
136
planning
2
2
2
2
2
0
qlock
36
36
36
36
36
0
RTCL
4
4
4
4
4
4
sal
10
10
10
10
10
8
sep
9
9
9
9
9
8
Total
770
514
586
658
665
319
Table 2. Results on Instance from SMTLIB-IDL
Fig. 3.
Fig. 3. Run time comparison on job shop scheduling instances.
Fig. 4.
Fig. 4. Run time comparison on Without Boolean category of SMTLIB-IDL.
7.3 Results on SMTLIB-IDL Benchmark Set (Table 2, Figure 4)
Similar to the case for SMTLIB-LIA, our local search solver shows the best performance on SMT(IDL) instances without Boolean variables (solving 687 out of the 841 instances), which can be seen from Table 2 and Figure 4. LocalSMT works particularly well on instances from “job_shop” and “jobshop(2022)”, which are job shop scheduling problem adopting the encoding method in [44]. The run time comparison on these types of instances is presented in Figure 3.
However, LocalSMT performs worse than its competitors on those With Boolean variables. Overall, LocalSMT cannot rival its competitors on this benchmark set, but works particularly well on the instances without Boolean variables.
Table 3.
Family
Type
#inst
MathSAT5
CVC5
Yices2
Z3
LocalSMT
Without Boolean
AProVE
1,676
1,647
1,373
1,593
1,658
1,627
CInteger
1,134
717
323
520
771
801
ITS
12,414
7,785
5,502
6,816
8,540
9,449
LassoRanker
4
4
4
4
4
4
leipzig
162
128
90
101
159
154
mcm
181
13
16
11
15
97
MathProblems(2022)
868
203
227
112
659
0
Total
16,439
10,497
7,535
9,157
11,806
12,132
With Boolean
calypto
80
78
79
79
80
32
Dartagnan(2021)
33
13
13
9
13
0
ezsmt(2019)
8
8
8
8
8
0
SAT14
1,853
1,801
1,802
1,840
1,852
1,633
UltimateLassoRanker
6
6
6
6
6
4
Total
1,980
1,906
1,908
1,942
1,959
1,669
Table 3. Results on Instances from SMTLIB-NIA
Fig. 5.
Fig. 5. Run time comparison on Without Boolean category of SMTLIB-NIA.
7.4 Results on SMTLIB-NIA Benchmark Set (Table 3, Figure 5)
Our LocalSMT solver shows overwhelming performance on SMT(NIA) instances without Boolean variables (solving 12,132 out of the 16,439 instances), which can be seen from Table 3 and Figure 5. Note that there exist too many instances, making the run time comparison on Without Boolean category in Figure 5 indistinct, and thus we present the run time distribution comparison with competitors in Figure 6. It works particularly well on “ITS” and “CInteger” instances, which are industrial instances for termination proving [48]. Moreover, LocalSMT can exclusively solve 75 “mcm” instances where no competitors can solve, which account for 41.4% of such type of instances.
LocalSMT performs extremely poorly on instances of “MathProblems(2022)” type, failing to solve any benchmark of this type, for the following reasons: First, the benchmark set contains hard mathematical problems such as sum of three cubes [71] and Magic squares of cubes [2], where the exponents on each variable is higher than 2. In this case, our solver cannot find any critical move operation as we only apply critical move when the exponent is not higher than 2, and thus it fails to find any solution. Moreover, these benchmarks have few clauses, which are not typical SMT formulas, and hence the local-search scoring function concerning the state of clauses will become ineffective.
On those SMT(NIA) instances with Boolean variables, LocalSMT performs overall worse than its competitors, but is still comparable. In general, LocalSMT can solve the most instances on SMTLIB-NIA.
7.5 Combination with Z3 and Summary on SMT-LIB Benchmark Sets (Table 4)
To confirm the complementarity of our local search solver with state-of-the-art SMT solvers, we combine LocalSMT with Z3, by running Z3 with a time limit of 600s, and then LocalSMT from scratch with the remaining 600s if Z3 fails to solve the instance. This wrapped solver can be regarded as a sequential portfolio solver, denoted as “Z3+LS”.
Fig. 6.
Fig. 6. Run time distribution comparison with competitor on Without Boolean category of SMTLIB-NIA.
Table 4.
#inst
MathSAT5
CVC5
Yices2
Z3
LocalSMT
Z3+LS
LIA_no_bool
6,670
6,442
6,242
5,994
6,385
6,478
6,536
LIA_with_bool
1,842
1,619
766
1,662
1,617
912
1,625
Total
8,512
8,061
7,008
7,656
8,002
7,390
8,161
IDL_no_bool
841
363
539
654
653
687
687
IDL_with_bool
770
514
586
658
665
319
661
Total
1,611
877
1,125
1,312
1,318
1,006
1,348
NIA_without_bool
16,439
10,497
7,535
9,157
11,806
12,132
12,946
NIA_with_bool
1,980
1,906
1,908
1,942
1,959
1,669
1,952
Total
18,419
12,403
9,443
11,099
13,765
13,801
14,898
Table 4. Summary Results on SMTLIB-LIA, SMTLIB-IDL and SMTLIB-NIA
Instances without and with Boolean variables are denoted by “no_bool” and “with_bool” respectively.
We summarize the results of all solvers, including Z3+LS, on 3 SMT-LIB benchmark sets in Table 4. Among all single-engine solvers, MathSAT5 solves the most instances of SMTLIB-LIA benchmark set, Z3 solves the most instances of SMTLIB-IDL benchmark set, while LocalSMT solves the most instances of SMTLIB-NIA benchmark set. Moreover, LocalSMT outperforms its competitors on instances without Boolean variables from all 3 benchmark sets, indicating that local search is an effective approach for solving SMT(IA) instances with only integer variables.
Fig. 7.
Fig. 7. Run time comparison between Z3+LS and default Z3 on all benchmarks.
Z3+LS solves more instances than any other solver on all benchmark sets, confirming that LocalSMT and Z3 have complementary performance and their combination pushes the state of the art in solving satisfiable instances of SMT(IA). We also combined LocalSMT with Yices in the same manner, resulting in a wrapped solver called YicesLS [16], which won the Single-Query and Model-Validation Track on QF_IDL in SMT-COMP 2021.
The run time comparison between Z3+LS and the default Z3 on all benchmarks is presented in Figure 7. Since the portfolio solver Z3+LS runs Z3 for the first 600s, Z3+LS and Z3 show the same performance in the first 600s, and thus we only compare two solvers on the remaining 600s. As shown in Figure 7, most points are concentrated on the top left side of the figure, indicating most instances which fails to be solved by Z3 can be solved fast once switching to running LocalSMT. Hence, this confirms that LocalSMT is complementary to state-of-the-art SMT solvers.
Note that in contrast to the delicate portfolio configuration of previous work where the cutoff time for the local search approach is parameterized over metrics depending on the input problem [56, 57], our portfolio configuration is set as basic as possible, because the main purpose of the portfolio configuration in this evaluation is to show that LocalSMT is indeed complimentary. We want to demonstrate that even though the portfolio configuration may not be the optimal setting, Z3+LS still outperforms all rivals, and it shows that LocalSMT is able to solve problems that can be considered hard for Z3 alone, confirming the complementarity of LocalSMT with state-of-the-art SMT solvers. Thus, we adopt a straightforward portfolio configuration, allocating equal time to both solvers. Since neither solvers interacts with the other, the order does not influence the number of solutions; hence, it does not matter whether to Z3 or LocalSMT is executed first.
Table 5.
Family
Type
#inst
bcl-maxsmt
bcl-ninc-cores
bcl-ninc
bcl-omt
bcl-cores
LocalSMT
Without Boolean
AProVE
1,676
1,662
1,663
1,663
1,648
1,663
1,627
CInteger
1,134
805
847
850
818
849
801
ITS
12,414
9,216
9,391
9,402
9,136
9,397
9,449
LassoRanker
4
4
4
4
4
4
4
leipzig
162
153
155
155
147
158
154
mcm
181
17
18
23
19
15
97
MathProblems(2022)
868
587
586
586
655
646
0
Total
16,439
12,444
12,664
12,683
12,427
12,732
12,132
With Boolean
calypto
80
80
80
80
80
80
32
Dartagnan(2021)
33
0
0
0
0
0
0
ezsmt(2019)
8
0
0
0
0
0
0
SAT14
1,853
1,853
1,853
1,853
1,853
1,853
1,633
UltimateLassoRanker
6
6
6
6
6
6
4
Total
1,980
1,939
1,939
1,939
1,939
1,939
1,669
Table 5. Comparison with Incomplete Solvers on SMTLIB-NIA
7.6 Comparison with Incomplete Solvers
We compare LocalSMT with 5 modified variants of the incomplete solver proposed in [9], where the SMT(NIA) problems are solved by reducing them to SMT(LIA). Note that instances from CInteger and ITS benchmark sets are generated by their constraint-based termination prover VeryMax [8] on the divisions of the termination competition termCOMP2016,10 taking up a large proportion of SMTLIB-NIA, amount to 77.2%.
The experimental results are shown in Table 5. LocalSMT is competitive but in general worse than the incomplete solvers, but it works particularly well on “mcm” type. The key weakness compared with the competitors lies in the “MathProblems(2022)” type, which has been proved above to be unsuitable for LocalSMT. Excluding the “MathProblems(2022)” type, LocalSMT can outperform all incomplete solver on the without Boolean category, which convinces again that LocalSMT performs particularly well on instances with only integer variables.
Note that there seems to be some issues in the incomplete solvers proposed in [8]. On 5 instances11 from “Dartagnan”, all modified variants of the incomplete solver report “UNSAT”, while 4 CDCL(T) competitors report “SAT”.
7.7 Effectiveness of Proposed Strategies
To analyze the effectiveness of the strategies in LocalSMT, we modify LocalSMT to obtain 5 alternative versions as follows:
—
To analyze the effectiveness of the cm operator, we modify LocalSMT by replacing the cm operator with the operator that directly modifies an integer variable by a fixed increment \(inc\), leading to two versions v_fix_1 and v_fix_5, where \(inc\) is set as 1 and 5 respectively.
—
To analyze the effectiveness of the two level heuristic for picking a decreasing cm operation, we modify LocalSMT by choosing a decreasing cm operation only from falsified clauses or directly from all false literals, leading to two versions, namely v_focused and v_extend.
—
To analyze the effectiveness of \(dscore\), we modify LocalSMT to choose a cm operation with the highest \(score\) from the selected clause at local optima, leading to the version v_score.
Fig. 8.
Fig. 8. Run time distribution comparison with modified version on SMTLIB-LIA.
Fig. 9.
Fig. 9. Run time distribution comparison with modified versions on SMTLIB-IDL.
Fig. 10.
Fig. 10. Run time distribution comparison with modified versions on SMTLIB-NIA.
We compare LocalSMT with these modified versions on the SMTLIB-LIA and SMTLIB-IDL benchmark sets. The runtime distribution of LocalSMT and its modified versions on the two benchmark sets are presented in Figures 8–10, confirming the effectiveness of the strategies. Note that instances which can be solved by all versions within 1 second are dismissed, specifically, such instances in SMTLIB-LIA, SMTLIB-IDL, and SMTLIB-NIA benchmark sets amount to 4759, 73 and 505, respectively.
From the runtime distribution comparison, we can conclude that critical move is the most important component to improve performance, because LocalSMT can significantly outperform v_fix_1 and v_fix_5. A possible explanation for the great promotion effect of critical move is that the search space of SMT(IA) is sparse, and thus modifying the variable to threshold can help the algorithm avoid getting stuck in a space without solution. The idea of two-level heuristic also plays an important role in our algorithm. Comparatively, the dscore is less effective, although it also contributes considerably to the SMTLIB-IDL instances. One explanation is that the calculation of dscore requires much overhead, which reduces the benefits it brings.
8 Conclusion and Future Work
We developed the first local search solver for SMT(IA), opening the local search direction for SMT on integer theories. Main features of our solver include a framework switching between Boolean and Integer modes, the critical move operator and a scoring function based on distance to satisfaction. Experiments show that our solver is competitive and complementary to state-of-the-art SMT solvers.
We would like to enhance our solver by improving the performance on instances with Boolean variables, and develop local search solver for SMT on real number theories. It is also interesting to explore deep cooperation with DPLL(T) solvers.
\(\lceil a \rceil\) returns the ceiling value which is the closest integer greater than or equal to a given number \(a\), while \(| a |\) denotes the absolute value of \(a\).
4
\(a\mid b\) means that \(b\) is divisible by \(a\).
S. Amin and J. L. Fernandez-Villacanas. 1997. Dynamic local search. In Proceedings of the 2nd International Conference On Genetic Algorithms In Engineering Systems: Innovations And Applications. 129–132. DOI:
Adrian Balint and Uwe Schöning. 2012. Choosing probability distributions for stochastic local search and the role of make versus break. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Springer, 16–29.
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A versatile and industrial-strength SMT solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 415–442.
Tewodros Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. 2014. A constraint-based approach to solving games on infinite graphs. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 221–233.
Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. 2017. Proving termination through conditional termination. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 99–117.
Cristina Borralleras, Daniel Larraz, Enric Rodríguez-Carbonell, Albert Oliveras, and Albert Rubio. 2019. Incomplete SMT techniques for solving non-linear formulas over the integers. ACM Transactions on Computational Logic 20, 4 (2019), 1–36.
Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. 2012. SAT modulo linear arithmetic for solving polynomial constraints. Journal of Automated Reasoning 48, 1 (2012), 107–131.
Martin Bromberger, Mathias Fleury, Simon Schwarz, and Christoph Weidenbach. 2019. SPASS-SATT. In Proceedings of the International Conference on Automated Deduction. Springer, 111–122.
Martin Bromberger and Christoph Weidenbach. 2016. Fast cube tests for LIA constraint solving. In Proceedings of the International Joint Conference on Automated Reasoning. Springer, 116–132.
Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia. 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Proceedings of the International Conference on Computer Aided Verification. Springer, 78–92.
Shaowei Cai. 2015. Balance between complexity and quality: Local search for minimum vertex cover in massive graphs. In Proceedings of the 24th International Joint Conference on Artificial Intelligence. 747–753.
Shaowei Cai, Bohan Li, and Xindi Zhang. 2022. Local search for SMT on linear integer arithmetic. In Proceedings of the International Conference on Computer Aided Verification. Springer, 227–248.
Shaowei Cai, Chuan Luo, and Kaile Su. 2015. CCAnr: A configuration checking based local search solver for non-random satisfiability. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Springer, 1–8.
Shaowei Cai and Kaile Su. 2012. Configuration checking with aspiration in local search for SAT. In Proceedings of the 26th AAAI Conference on Artificial Intelligence.
Shaowei Cai and Kaile Su. 2013. Local search for boolean satisfiability with configuration checking and subscore. Artificial Intelligence 204 (2013), 75–98.
Shaowei Cai, Kaile Su, and Abdul Sattar. 2011. Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artificial Intelligence 175, 9–10 (2011), 1672–1696.
Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. 2012. SMTInterpol: An interpolating SMT solver. In Proceedings of the International SPIN Workshop on Model Checking of Software. Springer, 248–254.
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013. The mathsat5 smt solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 93–107.
Michael A. Colón, Sriram Sankaranarayanan, and Henny B. Sipma. 2003. Linear invariant generation using non-linear constraint solving. In Proceedings of the International Conference on Computer Aided Verification. Springer, 420–432.
Scott Cotton, Andreas Podelski, and Bernd Finkbeiner. 2005. Satisfiability checking with difference constraints. IMPRS Computer Science, Saarbruceken (2005).
Bruno Dutertre and Leonardo De Moura. 2006. Integrating simplex with DPLL (T). Computer Science Laboratory, SRI International, Tech. Rep. SRI-CSL-06-01 (2006).
Bruno Dutertre and Leonardo de Moura. 2006. A fast linear-arithmetic solver for DPLL (T). In Proceedings of the International Conference on Computer Aided Verification. Springer, 81–94.
Andreas Fröhlich, Armin Biere, Christoph Wintersteiger, and Youssef Hamadi. 2015. Stochastic local search for satisfiability modulo theories. In Proceedings of the AAAI 2015.
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl. 2007. SAT solving for termination analysis with polynomial interpretations. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Springer, 340–354.
Malay K. Ganai, Muralidhar Talupur, and Aarti Gupta. 2006. SDSAT: Tight integration of small domain encoding and lazy approaches in a separation logic solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 135–150.
Natalia Gavrilenko, Hernán Ponce-de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. 2019. BMC for weak memory models: Relation analysis for compact SMT encodings. In Proceedings of the International Conference on Computer Aided Verification. Springer, 355–365.
Alberto Griggio. 2012. A practical approach to satisfiability modulo linear integer arithmetic. Journal on Satisfiability, Boolean Modeling and Computation 8, 1–2 (2012), 1–27.
Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, and Silvia Tomasi. 2011. Stochastic local search for SMT: Combining theory solvers with walksat. In Proceedings of the International Symposium on Frontiers of Combining Systems. Springer, 163–178.
Frank Hutter, Dave A. D. Tompkins, and Holger H. Hoos. 2002. Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In Principles and Practice of Constraint Programming-CP 2002: 8th International Conference, CP 2002 Ithaca, NY, USA, September 9–13, 2002 Proceedings 8. Springer, 233–248.
Tomi Janhunen, Ilkka Niemelä, and Mark Sevalnev. 2009. Computing stable models via reductions to difference logic. In Proceedings of the LPNMR 2009. Springer, 142–154.
Dejan Jovanović. 2017. Solving nonlinear integer arithmetic with MCSAT. In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 330–346.
Dejan Jovanovic, Clark Barrett, and Leonardo De Moura. 2013. The design and implementation of the model constructing satisfiability calculus. In Proceedings of the 2013 Formal Methods in Computer-Aided Design. IEEE, 173–180.
Hyondeuk Kim, Hoonsang Jin, and Fabio Somenzi. 2007. Disequality management in integer difference logic via finite instantiations. Journal on Satisfiability, Boolean Modeling and Computation 3, 1–2 (2007), 47–66.
Tim King, Clark Barrett, and Bruno Dutertre. 2013. Simplex with sum of infeasibilities for SMT. In Proceedings of the 2013 Formal Methods in Computer-Aided Design. IEEE, 189–196.
Gereon Kremer, Florian Corzilius, and Erika Ábrahám. 2016. A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. In Proceedings of the International Workshop on Computer Algebra in Scientific Computing. Springer, 315–335.
Wolfgang Kunz and Dominik Stoffel. 1997. Reasoning in Boolean Networks: Logic Synthesis and Verification using Testing Techniques. Vol. 9. Springer Science & Business Media.
Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. 2014. Proving non-termination using Max-SMT. In Proceedings of the International Conference on Computer Aided Verification. Springer, 779–796.
Chu Min Li and Yu Li. 2012. Satisfying versus falsifying in local search for satisfiability. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Springer, 477–478.
Nuno P. Lopes and José Monteiro. 2016. Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. International Journal on Software Tools for Technology Transfer 18, 4 (2016), 359–374.
Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340.
Leonardo de Moura and Dejan Jovanović. 2013. A model-constructing satisfiability calculus. In Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 1–12.
Aina Niemetz and Mathias Preiner. 2020. Ternary propagation-based local search for more bit-precise reasoning. In # PLACEHOLDER_PARENT_METADATA_VALUE#, Vol. 1. TU Wien Academic, 214–224.
Aina Niemetz, Mathias Preiner, and Armin Biere. 2016. Precise and complete propagation based local search for satisfiability modulo theories. In Proceedings of the International Conference on Computer Aided Verification. Springer, 199–217.
Aina Niemetz, Mathias Preiner, and Armin Biere. 2017. Propagation based local search for bit-precise reasoning. Formal Methods in System Design 51, 3 (2017), 608–636.
Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. 2006. Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL (T). Journal of the ACM 53, 6 (2006), 937–977.
André Platzer, Jan-David Quesel, and Philipp Rümmer. 2009. Real world verification. In Proceedings of the International Conference on Automated Deduction. Springer, 485–501.
Amir Pnueli, Yoav Rodeh, Ofer Strichman, and Michael Siegel. 2002. The small model property: How small can it be? Information and Computation 178, 1 (2002), 279–293.
Sabino Francesco Roselli, Kristofer Bengtsson, and Knut Åkesson. 2018. SMT solvers for job-shop scheduling problems: Models comparison and performance evaluation. In Proceedings of the 2018 IEEE 14th International Conference on Automation Science and Engineering. IEEE, 547–552.
Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. 2004. Constructing invariants for hybrid systems. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control. Springer, 539–554.
Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. 2004. Non-linear loop invariant generation using Gröbner bases. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 318–329.
Bart Selman, Henry A. Kautz, Bram Cohen, et al. 1993. Local search strategies for satisfiability testing. Cliques, Coloring, and Satisfiability 26 (1993), 521–532.
Sanjit A. Seshia, Shuvendu K. Lahiri, and Randal E. Bryant. 2003. A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In Proceedings of the 2003. Design Automation Conference. IEEE, 425–430.
Ofer Strichman, Sanjit A. Seshia, and Randal E. Bryant. 2002. Deciding separation formulas with SAT. In Proceedings of the International Conference on Computer Aided Verification. Springer, 209–222.
Muralidhar Talupur, Nishant Sinha, Ofer Strichman, and Amir Pnueli. 2004. Range allocation for separation logic. In Proceedings of the International Conference on Computer Aided Verification. Springer, 148–161.
John Thornton, Duc Nghia Pham, Stuart Bain, and Valnir Ferreira Jr. 2004. Additive versus multiplicative clause weighting for SAT. In AAAI 4, (2004), 191–196.
ICSE '24: Proceedings of the IEEE/ACM 46th International Conference on Software Engineering
Satisfiability Modulo Theory (SMT) generalizes the propositional satisfiability problem (SAT) by extending support for various first-order background theories. In this paper, we focus on the SMT problems in Non-Linear Integer Arithmetic (NIA) theory, ...
Satisfiability Modulo Linear Integer Arithmetic, SMT (LIA) for short, has significant applications in many domains. In this paper, we develop the first local search algorithm for SMT (LIA) by directly operating on variables, breaking through the ...
AAAI'15: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence
Satisfiability Modulo Theories (SMT) is essential for many practical applications, e.g., in hard- and software verification, and increasingly also in other scientific areas like computational biology. A large number of applications in these areas ...
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences and School of Computer Science and Technology, University of Chinese Academy of Sciences, China
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences and School of Computer Science and Technology, University of Chinese Academy of Sciences, China
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences and School of Computer Science and Technology, University of Chinese Academy of Sciences, China
