VolCE: An E cient Tool for Solving #SMT(LA) Problems

Abstract

We present VolCE, a tool for computing and estimating the size of the solution space of SMT(LA) constraints. VolCE supports the SMT-LIB format. It integrates SMT solving with volume computation/estimation and integer solution counting for convex polytopes. Several e ective techniques are adopted, which enable the tool to deal with high-dimensional problem instances e ciently.

Introduction

In recent years, there have been a lot of works on solving the Satis ability Modulo Theories (SMT) problem. Quite e cient SMT solvers have been developed, such as CVC3, Z3 and Yices [ 1, 5, 7 ]. In [ 17, 10 ], we studied the counting version of SMT solving, and presented some techniques for computing the size of the solution space e ciently. This problem can be regarded as an extension to SMT solving, and also an extension to model counting in the propositional logic. Its interesting applications in several elds include program analysis [ 15, 11, 12 ], probabilistic inference [ 18, 4 ], planning [ 6 ] and privacy/con dentiality veri cation [ 8 ].

This paper presents the tool VolCE4 for the counting version of SMT(LA)5. The input of the tool is an SMT(LA) formula. The output of the tool is the \volume" of the solution space, or the number of solutions in case that the domains (of variables) are all discrete. VolCE supports the SMT-LIB (v2.0) format which is a common language to describe SMT formulas. It is an integration of SMT solving and polytope subroutines, such as, volume computation, volume estimation and integer point counting for convex polytopes. Moreover, VolCE adopts bunch and cache strategy to reduce the number of calls of polytope subroutines, and employs several more techniques to reduce the di culty of polytope subroutines. As a result, the tool is enabled to deal with high-dimensional problem instances e ciently. 4 Our tool VolCE is available at http://www.github.com/bearben/volce 5 Here LA stands for linear arithmetic. So LIA and LRA stands for linear integer arithmetic and linear real arithmetic respectively.

Background

This section provides brief overviews of SMT(LA) formulas and convex polytopes as far as is needed to make this paper self-contained.

An SMT formula over linear inequalities, i.e., an SMT(LA) formula, can be represented as a Boolean formula P S (b1; : : : ; bn) together with de nitions in the form: bi ci. Here cis are linear inequalities. P S is the propositional skeleton of the formula .

Let us consider two speci c types of numeric variables, the integers and reals. There are SMT(LIA) formulas and SMT(LRA) formulas. For an SMT(LIA) formula, we count the number of solutions. For an SMT(LRA) formula, we compute the volume of the solution space instead. The assignment of the propositional skeleton of the SMT(LA) formula corresponds to a conjunction of linear inequalities which can be regarded as a convex polytope.

Tools for Polytope Subroutines. To describe VolCE, we introduce the following three tools, which are also called polytope subroutines: { PolyVest. In [ 9, 10 ], we introduced a probabilistic algorithm for volume estimation on convex polytopes. A tool called PolyVest was implemented which can give results with ( ; )-bound, i.e., for a given polytope P , PolyVest returns an estimation that lies in the interval [(1 + ) 1#P; (1 + )#P ] with probability at least 1 , where #F is the exact volume of P . It can e ciently handle polytopes with dozens of dimensions. { Vinci. Before PolyVest, there was already a tool available called Vinci [ 2 ] which can compute the volume of a convex polytope. It gives the exact volume instead of an estimation. The input of Vinci should be a set of LRA constraints. { LattE. LattE [ 16 ] is a tool dedicated to the counting of lattice points inside convex polytopes. It requires the input polytopes in the integer matrix A and vector b. 3

Architecture

VolCE has the following three functions: { Estimate volume for SMT(LRA) formulas; { Compute volume for SMT(LRA) formulas; { Count the number of lattice points for SMT(LIA) formulas.

The basic idea of VolCE is to enumerate feasible assignments by solving the SMT(LA) formula and accumulate the volumes of these assignments. Polytope volume computation/estimation (or lattice counting) serves as a subroutine which produces the volume (or solution count) of each feasible assignment. A schematic overview is shown in Fig. 1. A regular run of VolCE has three stages: parsing and rewriting, feasible assignments enumeration and polytope subroutines.

SMT-LIB Input Volume or #Solutions Parser Inequality Extractor Parsing and rewritting

Bunch

Generation SMT(LA) Solver, e.g. Z3

Feasible assignements enumeration 1-dim

Problem

Interval Computation Compute & Update

Polytope Preprocessing

Search

Two-round

Strategy Cache

PolyVest Vinci

LattE Polytope subroutines: volume estimation, volume

computation, lattice counting The parser reads the input and recursively builds an abstract syntax DAG (directed acyclic graph). Like most SMT solvers, basic rewriting rules are applied to simplify the DAG during the parsing process.

Inequality Extraction. VolCE is essentially a divide-and-conquer algorithm. It partitions the solution space of an SMT(LA) formula into polytopes and calls polytope subroutines to handle each polytope. Recall that polytope subroutines only take linear inequalities as inputs, so VolCE has to extract inequalities from SMT(LA) formulas. The inequality extractor is a component to rewrite the SMT(LA) expression into a combination of Boolean skeletons and normalized linear inequalities. Parser calls extractor whenever it has parsed a comparison operator (=; <; ; >; , distinct) which is the root of a DAG of inequalities. Note that such a DAG may consist of more than one inequality if it contains ite operators. For a DAG with ites, the extractor recursively traverses the DAG, records the conditions of each ite and then reconstructs a syntax tree with Boolean variables which represents those extracted inequalities. Each time an inequality is extracted, VolCE creates a Boolean variable to substitute this inequality in the DAG and adds a constraint to link the variable with the inequality.

Inequality Normalization. The extraction procedure also normalizes inequalities. With Boolean operations, one can represent <; ; > and simply by , e.g., x + y < 0 , not (x + y 0) , not ( x y 0). Thus a normalized inequality is of the form a0 + a1x1 + : : : + anxn = ( ) 0, where ais are constants, xis are variables, and a0 0. 3.2

Feasible Assignments Enumeration

In the second stage, VolCE tries to enumerate all feasible assignments. It calls the SMT solver to obtain a feasible assignment, then adds a constraint to rule out the assignment just found, and so forth. VolCE currently uses Z3, as the SMT(LA) solver, through APIs. Note that it is easy to employ other modern SMT solvers since VolCE sees SMT solving as a black box.

Bunch Strategy [ 17 ]. To reduce the number of calls of polytope subroutines, we proposed a strategy in [ 17 ] that combines the feasible assignments into \bunches". Each time a feasible assignment is obtained, we search the neighbourhood of this assignment by negating its literals. We can combine the original assignment with one of its feasible neighbour assignments. Then we obtain a partial assignment that still propositionally satis es the formula. The resulting assignment may cover a bunch of feasible assignments, hence is called a \bunch". The polytope subroutine is called for the polytope corresponding to each bunch rather than each feasible assignment, so that the number of calls is reduced. 3.3

Polytope Subroutines

In the third stage, VolCE calls polytope subroutines for each bunch to obtain the volume or the solution count, and then sums up. Recall that VolCE has three functions, so there are three polytope subroutines: (i) polytope volume estimation with tool PolyVest, (ii) polytope volume computation with tool Vinci, and (iii) polytope lattice couting with tool LattE. Recall that PolyVest produces estimation with ( ; )-bound. Since VolCE simply sums up the estimations from PolyVest, the volume estimation presented by VolCE also satis es ( ; )-bound. As a result, VolCE has two command-line parameters -epsilon and -delta to control the accuracy of the volume estimation.

Polytope subroutines are time-consuming and usually the bottleneck of the whole program. VolCE employs a new cache strategy to reuse the results of polytope subroutines. VolCE also integrates techniques proposed in [ 10 ] to detect and solve cases which frequently occur in #SMT problems but ine ciently handled by polytope subroutines.

Reusing with Cache. VolCE stores the results of calls of polytope subroutines in a cache, so that it can retrieve the result of a problem which has already been solved from the cache. Each call of a polytope subroutine corresponds to a polytope. Because VolCE has extracted and stored all inequalities, the polytope passed to a polytope subroutine is essentially an assignment of inequalities. So we set the assignment of inequalities to be the key and bind it to the results returned by the polytope subroutine. For SMT(LA) formulas without free Boolean variables, the conjunctions of inequalities under di erent feasible assignments should be disjoint with each other. However, it is common that an SMT(LA) formula contains free Boolean variables. In this case, di erent feasible assignments may correspond to the same polytope. Besides, polytope partition techniques could partition di erent polytopes into the same sub-dimensional polytope. Polytope Preprocessing [ 10 ]. The number of variables is a key factor about the di culty of a polytope subroutine. VolCE employs polytope preprocessing techniques for dimension reduction. VolCE rst partitions the set of linear inequalities, which corresponds to a given bunch, into mutually independent groups of inequalities, then applies the polytope subroutine to obtain the size of solution space of each group of inequalities, and nally returns the multiplications. VolCE also tries to check and reduce irrelevant variables whenever it calls polytope subroutine.

Two-round Strategy [ 10 ]. As the number of random points increases, the accuracy of estimation improves, and the estimation process also takes more time. It is important to balance the accuracy and the running time since the estimation subroutine is usually called many times. Therefore, VolCE employs a two-round strategy [ 10 ] that can dynamically determine a proper weight for each feasible (partial) assignment. 4

Experimental Results

In this section, we report experimental results about the performance of VolCE. VolCE provides a command-line parameter -w to quickly set bounds to numeric variables. Speci cally, with such word-length parameter w, VolCE bounds each variable in the domain [ 2w 1; 2w 1 1]. We set w = 8, = 0:5 and = 0:1 for experiments on SMT(LRA) formulas. The settings of w on SMT(LIA) formulas are listed with experimental results. The experiments are conducted on a workstation with 3.40GHz Intel Core i7-2600 CPU and 8GB memory. The test cases 6 (more than 300) include: { Random instances lra b n l: which have b Boolean variables, n real variables and l inequalities. They are generated by randomly choosing coe cients of inequalities and literals of clauses. { Random instances lia b n l: which are similar to lra b n l but are SMT(LIA) formulas. { Instances generated from static program analysis. We analyzed the following programs: (i) abs: a function which calculates absolute values; (ii) findmiddle: a function which nds the middle number among 3 numbers; (iii) Space manage: a program related to space technology; (iv) tritype: a program which determines the type of a triangle; (v) calDate: a function which converts the special date into a Julian date; (vi) tcas: a program about the tra c collision avoidance system; (vii) FINDpath: a selection program FIND [ 13 ]; (viii) getopPath: a program function called getop() [ 14 ].

In the following tables, \||" means that the instance takes more than one hour to solve (or the tool runs out of memory).

Table 1 presents the performance results of volume estimation and computation functions of VolCE on SMT(LRA) formulas. For lack of space, only a part 6 The set of benchmarks is available at http://www.github.com/bearben/volce of results are listed here. In Table 1, column 1 gives the instance name, column 2 the number of feasible assignments and column 3 the number of bunches enumerated by VolCE. Column 4 to 8 give the results of volume estimation function which correspond to the number of polytopes which are partitioned, the number of calls of estimation subroutine, the average number of dimensions of problems handled by polytope estimation subroutine, the outputs and the running times, respectively. Column 9 to 14 give the results of volume computation function. Note that column 11 presents the number of solutions reused.

The results in Table 1 show that VolCE can solve random instances with over 20-dimensions in reasonable time. Compared with the volume estimation function, the volume computation is more e cient on small instances. We observe that for all the benchmarks, VolCE gives estimations within the tolerance .

In addition, we nd that the bunch strategy works well. The feasible assignments are reduced by half on most of instances. Table 1 also shows that the solution reuse technique works on some instances and sometimes very e ective, e.g., \lra 20 20 10" and \lra 15 15 7". Note that the reuse technique is currently not available to the volume estimation function. Besides, the results show that polytope partition technique is useful on both functions. Due to the tworound strategy, the number of polytopes partitioned during volume estimation is sometimes more than the number of bunches.

To evaluate the performance of VolCE for solution counting, we compare it with SMTApproxMC [ 3 ] which is a state-of-the-art hashing-based approximate counter for SMT(BV) formulas. For comparison, we transformed SMT(LIA) formulas into SMT(BV) formulas manually by replacing integer variables with xed-length variables, bit-vector constants and bit operations. We experimented SMTApproxMC with parameters = 0:8 and = 0:2. It guarantees the output lying in interval [1:8 1RF ; 1:8RF ] with probability at least 80%, where RF is the real count of a given formula F . large class of benchmarks. We observe that the running time of SMTApproxMC is closely related to the number of the solutions rather than the number of variables, i.e., the larger number of solutions, the more di cult for SMTApproxMC to handle. Besides, the results on industry instances demonstrate that our tool is potentially useful in program analysis. 5

Concluding Remarks

VolCE is a tool for computing and estimating the volume of the solution space (or counting the number of solutions), given a formula/constraint which is a Boolean combination of linear arithmetic inequalities. For medium sized SMT(LA) formulas, it can provide exact volume computation results or exact number of solutions. For larger SMT(LRA) formulas, it can perform volume estimation with high accuracy, due to the use of e ective heuristics. We believe that the tool will be useful in a number of domains, such as program analysis and probabilistic veri cation.

References

1. C. Barrett , C. L. Conway , M. Deters , L. Hadarean , D. Jovanovic , T. King , A. Reynolds , and C. Tinelli . CVC4. In Proc. of CAV , pages 171 { 177 , 2011 .

2. B. Bu eler, A. Enge , and K. Fukuda . Exact Volume Computation for Polytopes: A Practical Study , pages 131 { 154 . Birkhauser Basel, 2000 .

3. S. Chakraborty , K. S. Meel , R. Mistry , and M. Y. Vardi . Approximate probabilistic inference via word-level counting . In Proc. of AAAI , pages 3218 { 3224 , 2016 .

4. M. Chavira and A. Darwiche . On probabilistic inference by weighted model counting . Artif . Intell., 172 ( 6-7 ): 772 { 799 , 2008 .

5. L. M. de Moura and N. Bj rner. Z3: an e cient SMT solver . In Proc. of TACAS , pages 337 { 340 , 2008 .

6. C. Domshlak and J. Ho mann. Probabilistic planning via heuristic forward search and weighted model counting . J. Artif. Intell. Res. (JAIR) , 30 : 565 { 620 , 2007 .

7. B. Dutertre . Yices 2.2 . In Proc. of CAV , pages 737 { 744 , 2014 .

8. M. Fredrikson and S. Jha . Satis ability modulo counting: a new approach for analyzing privacy properties . In Proc. of CSL-LICS , pages 42 :1{ 42 : 10 , 2014 .

9. C. Ge and F. Ma . A fast and practical method to estimate volumes of convex polytopes . In Proc. of FAW , pages 52 { 65 , 2015 .

10. C. Ge , F. Ma , P. Zhang, and J. Zhang. Computing and estimating the volume of the solution space of SMT(LA) constraints . Accepted to appear in TCS, http://dx.doi.org/10.1016/j.tcs. 2016 . 10 .019.

11. J. Geldenhuys , M. B. Dwyer , and W. Visser . Probabilistic symbolic execution . In Proc. of ISSTA , pages 166 { 176 , 2012 .

12. K. Gleissenthall , B. Kopf, and A. Rybalchenko . Symbolic polytopes for quantitative interpolation and veri cation . In Proc. of CAV , pages 178 { 194 , 2015 .

13. C. A. R. Hoare . Proof of a program: FIND. Commun . ACM, 14 ( 1 ): 39 { 45 , 1971 .

14. B. W. Kernighan. The C Programming Language . Prentice Hall Professional Technical Reference, 2nd edition , 1988 .

15. S. Liu and J. Zhang. Program analysis: from qualitative analysis to quantitative analysis . In Proc. of ICSE , pages 956 { 959 , 2011 .

16. J. A. De Loera , R. Hemmecke , J. Tauzer , and R. Yoshida . E ective lattice point counting in rational convex polytopes . J. Symb. Comput. , 38 ( 4 ): 1273 { 1302 , 2004 .

17. F. Ma , S. Liu, and J. Zhang. Volume computation for boolean combination of linear arithmetic constraints . In Proc. of CADE , pages 453 { 468 , 2009 .

18. D. Roth . On the hardness of approximate reasoning . Artif. Intell., 82 ( 1-2 ): 273 { 302 , 1996 .