6 Years of SMT-COMP

The annual Satisfiability Modulo Theories Competition (SMT-COMP) was initiated in 2005 in order to stimulate the advance of state-of-the-art techniques and tools developed by the Satisfiability Modulo Theories (SMT) community. This paper summarizes the first six editions of the competition. We present the evolution of the competition’s organization and rules, show how the state of the art has improved over the course of the competition, and discuss the impact SMT-COMP has had on the SMT community and beyond. Additionally, we include an exhaustive list of all competitors, and present experimental results showing significant improvement in SMT solvers during these six years. Finally, we analyze to what extent the initial goals of the competition have been achieved, and sketch future directions for the competition.     

Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)

The Satisfiability Modulo Theories Competition (SMT-COMP) arose from the SMT-LIB initiative to spur adoption of common, community-designed formats, and to spark further advances in satisfiability modulo theories (SMT). The first SMT-COMP was held in 2005 as a satellite event of CAV 2005. SMT-COMP 2006 was held August 17–19, 2006, as a satellite event of CAV 2006. This paper describes the rules and competition format for SMT-COMP 2006, the benchmarks used, the participants, and the results.     

A parsimony tree for the SAT2002 competition

Twenty of the programs (solvers) submitted to the SAT 2002 Contest had no disqualifying errors. These solvers were run on 2023 satisfiability problems of varying hardnesses. Each solver was judged by which problems it could solve within the allowed time limit. Twelve solvers were best on some problem — they could solve it and the others could not. Only two solvers could not beat each remaining solver on some problems (where the problems could vary depending on which solver it was trying to beat). Thus, there is evidence that 18 solvers were extremely good. It is interesting to analyze the contest results in a way that groups together solvers with similar strengths and weaknesses. This paper uses the parsimony algorithm to produce a classification of the twenty solvers. The paper also has a second classification, almost the same as the first, for the twenty solvers, updated versions of two solvers, and a fictitious state of the art solver. The contest problems came in three groups, Industrial, Hand Made, and Random. The Random group of problems was about three times as large as the other two together. The classification identifies four groups of solvers (plus a miscellaneous group): weak solvers, incomplete solvers which are very good at some satisfiable Random problems, complete solvers which are very good at most Random problems, and complete solvers which are very good at Industrial and Hand Made problems.     

A parsimony tree for the SAT2002 competition

Twenty of the programs (solvers) submitted to the SAT 2002 Contest had no disqualifying errors. These solvers were run on 2023 satisfiability problems of varying hardnesses. Each solver was judged by which problems it could solve within the allowed time limit. Twelve solvers were best on some problem – they could solve it and the others could not. Only two solvers could not beat each remaining solver on some problems (where the problems could vary depending on which solver it was trying to beat). Thus, there is evidence that 18 solvers were extremely good. It is interesting to analyze the contest results in a way that groups together solvers with similar strengths and weaknesses. This paper uses the parsimony algorithm to produce a classification of the twenty solvers. The paper also has a second classification, almost the same as the first, for the twenty solvers, updated versions of two solvers, and a fictitious state of the art solver. The contest problems came in three groups, Industrial, Hand Made, and Random. The Random group of problems was about three times as large as the other two together. The classification identifies four groups of solvers (plus a miscellaneous group): weak solvers, incomplete solvers which are very good at some satisfiable Random problems, complete solvers which are very good at most Random problems, and complete solvers which are very good at Industrial and Hand Made problems.     

A personal perspective on problem solving by general purpose solvers

To solve the problems that abound in real‐world applications, we are proposing an approach of using general‐purpose solvers, as we cannot afford to develop special‐purpose algorithms for all individual problems. The existing general‐purpose solvers such as linear programming and integer programming are very useful but not sufficient. To improve the situation, we have developed solvers for other standard problems such as the constraint satisfaction problem and the resource‐constrained project scheduling problem among others. In this article, we describe why general‐purpose solvers are needed, what kinds of solvers we considered, how they were developed and where they have been applied.     

Strategic effort allocation in online innovation tournaments

Online innovation tournaments, such as those hosted by crowdsourcing platforms (e.g., Kaggle), have been widely adopted by firms to evolve creative solutions to various problems. Solvers compete in these tournaments to earn rewards. In such competitive environments, it is imperative that solvers provide creative solutions with minimum effort. This article explores the factors that influence the solvers’ effort allocation decisions in a dynamic tournament setting. Specifically, comprehensive time variant data of teams that participated in crowdsourcing competitions on Kaggle were analyzed to gain insight into how solvers continually formulate strategies in light of performance feedback obtained through interim ranking. The results suggest that solvers strategically allocate their efforts throughout the contest to dynamically optimize their payoffs through balancing the probability of winning and the cost of expending effort. In particular, solvers tend to increase their efforts toward the end of tournaments or when they get closer to winning positions. Furthermore, our findings indicate that a last-minute surge in effort is more prevalent among high-skill solvers than in those with lower skill levels. In addition to providing insights that may help solvers develop strategies to improve their performance, the study has implications for the design of online crowdsourcing platforms, particularly in terms of incentivizing solvers to put forth their best effort.     

Randomized constraint solvers: a comparative study

The complexity of constraints is a major obstacle for constraint-based software verification. Automatic constraint solvers are fundamentally incomplete: input constraints often build on some undecidable theory or some theory the solver does not support. This paper proposes and evaluates several randomized solvers to address this issue. We compared the effectiveness of a symbolic solver (CVC3), a random solver, two heuristic search solvers, and seven hybrid solvers (i.e. mix of random, symbolic, and heuristic solvers). We evaluated the solvers on a benchmark generated with a concolic execution of 9 subjects. The performance of each solver was measured by its precision, which is the fraction of constraints that the solver can find solution out of the total number of constraints that some solver can find solution. As expected, symbolic solving subsumes the other approaches for the 4 subjects that only generate decidable constraints. For the remaining 5 subjects, which contain undecidable constraints, the hybrid solvers achieved the highest precision (fraction of constraints that a solver can find a solution out of the total number of satisfiable constraints). We also observed that the solvers were complementary, which suggests that one should alternate their use in iterations of a concolic execution driver.     

Cuts from proofs: a complete and practical technique for solving linear inequalities over integers

We propose a novel, sound, and complete Simplex-based algorithm for solving linear inequalities over integers. Our algorithm, which can be viewed as a semantic generalization of the branch-and-bound technique, systematically discovers and excludes entire subspaces of the solution space containing no integer points. Our main insight is that by focusing on the defining constraints of a vertex, we can compute a proof of unsatisfiability for the intersection of the defining constraints and use this proof to systematically exclude subspaces of the feasible region with no integer points. We show experimentally that our technique significantly outperforms the top four competitors in the QF-LIA category of the SMT-COMP ’08 when solving conjunctions of linear inequalities over integers.     

On Modern Clause-Learning Satisfiability Solvers

In this paper, we present a perspective on modern clause-learning SAT solvers that highlights the roles of, and the interactions between, decision making and clause learning in these solvers. We discuss two limitations of these solvers from this perspective and discuss techniques for dealing with them. We show empirically that the proposed techniques significantly improve state-of-the-art solvers.     

Automatic Implication Checking for CHR Constraints

Constraint Handling Rules (CHRs) are a high-level rule-based programming language commonly used to define constraint solvers. We present a method for automatic implication checking between constraints of CHR solvers. Supporting implication is important for implementing extensible solvers and reification, and for building hierarchical CHR constraint solvers. Our method does not copy the entire constraint store, but performs the check in place using a trailing mechanism. The necessary code enhancements can be done by automatic program transformation based on the rules of the solver. We extend our method to work for hierarchically organized modular CHR solvers. We show the soundness of our method and its completeness for a restricted class of canonical solver as well as for specific existing non-canonical CHR solvers. We evaluate our trailing method experimentally by comparing with the copy approach: runtime is almost halved.     

A comparison of numerical methods for solving diffusion-reaction equations in air quality models

In this paper we analyze the efficiency of some stiff ode solvers, applied to the coupled solution of vertical turbulent diffusion and chemical kinetics in Air Quality Models. We consider four general-purpose solvers, based on bdf or Rosenbrock methods, and two special-purpose solvers, developed for odes from atmospheric chemistry, and compare their performance on three test problems using different chemical models. The general-purpose solvers have been modified to take advantage of the sparsity of the Jacobian matrices arising in the application of implicit methods. The obtained results show that general-purpose solvers, provided with suitable sparse matrix techniques, perform generally better than special-purpose ones. Our analysis extends to the diffusion-reaction equations the recent work of other research groups, comparing ode solvers on atmospheric chemical kinetics equations. Received: 28 January 1998 / Accepted: 26 April 1999     

Shape reanalysis and sensitivities utilizing preconditioned iterative boundary solvers

The computational advantages associated with the utilization of preconditioned iterative equation solvers are quantified for the reanalysis of perturbed shapes using continuum structural boundary element analysis (BEA). Both single- and multizone three-dimensional problems are examined. Significant redutions in computer time are obtained by making use of previously computed solution vectors and preconditioners in subsequent analyses. The effectiveness of this technique is demonstrated for the computation of shape response sensitivities required in shape optimization. Computer times and accuracies achieved using the preconditioned iterative solvers are compared with those obtained via direct solvers and implicit differentiation of the boundary integral equations. It is concluded that this approach employing preconditioned iterative equation solvers in reanalysis and sensitivity analysis can be competitive with if not superior to those involving direct solvers.     

Algorithm portfolios for noisy optimization

Noisy optimization is the optimization of objective functions corrupted by noise. A portfolio of solvers is a set of solvers equipped with an algorithm selection tool for distributing the computational power among them. Portfolios are widely and successfully used in combinatorial optimization. In this work, we study portfolios of noisy optimization solvers. We obtain mathematically proved performance (in the sense that the portfolio performs nearly as well as the best of its solvers) by an ad hoc portfolio algorithm dedicated to noisy optimization. A somehow surprising result is that it is better to compare solvers with some lag, i.e., propose the current recommendation of best solver based on their performance earlier in the run. An additional finding is a principled method for distributing the computational power among solvers in the portfolio.     

Element by element solvers of order N

A new family of higher order element by element (EBE) solvers possessing an improved accuracy is presented. These solvers are found to be consistently covergent, even for static one dimensional structural problems which are known to be troublesome for EBE solvers. The new EBE solvers, implemented together with the PCG method, are able to produce very accurate solutions for static structural problems.     

On the power of clause-learning SAT solvers as resolution engines

In this work, we improve on existing results on the relationship between proof systems obtained from conflict-driven clause-learning SAT solvers and general resolution. Previous contributions such as those by Beame et al. (2004), Hertel et al. (2008), and Buss et al. (2008) demonstrated that variations on conflict-driven clause-learning SAT solvers corresponded to proof systems as powerful as general resolution. However, the models used in these studies required either an extra degree of non-determinism or a preprocessing step that is not utilized by state-of-the-art SAT solvers in practice. In this paper, we prove that conflict-driven clause-learning SAT solvers yield proof systems that indeed p-simulate general resolution without the need for any additional techniques. Moreover, we show that our result can be generalized to certain other practical variations of the solvers, which are based on different learning schemes and restart policies.     

Accelerating iterative linear solvers using multiple graphical processing units

In this paper, we develop, study and implement iterative linear solvers and preconditioners using multiple graphical processing units (GPUs). Techniques for accelerating sparse matrix–vector (SpMV) multiplication, linear solvers and preconditioners are presented. Four Krylov subspace solvers, a Neumann polynomial preconditioner and a domain decomposition preconditioner are implemented. Our numerical tests with NVIDIA C2050 GPUs show that the SpMV kernel can be sped over 40 times faster using four GPUs. Our linear solvers and preconditioners have similar speedup.     

Solvers’ participation in crowdsourcing platforms: Examining the impacts of trust,and benefit and cost factors

Organizations are increasingly crowdsourcing their tasks to unknown individual workers, i.e., solvers. Solvers' participation is critical to the success of crowdsourcing activities. However, challenges exist in attracting solvers to participate in crowdsourcing. In this regard, prior research has mainly investigated the influences of benefit factors on solvers’ intention to participate in crowdsourcing. Thus, there is a lack of understanding of the cost factors that influence actual participation behavior, in conjunction with the benefits. Additionally, the role of trust in the cost-benefit analysis remains to be explored. Motivated thus, based on social exchange theory and context-related literature, we develop a model to explain the impacts of benefit and cost factors as well as trust on solver participation behavior in crowdsourcing. The model was tested using survey and archival data from 156 solvers on a large crowdsourcing platform. As hypothesized, monetary reward, skill enhancement, work autonomy, enjoyment, and trust were found to positively affect solvers’ participation in crowdsourcing, while cognitive effort negatively affects their participation. In addition, it was found that monetary reward positively affects trust (trust partially mediates its effect on participation behavior), while loss of knowledge power negatively affects trust. The theoretical contributions and practical implications of the study are discussed.     

An overview of parallel SAT solving

Boolean satisfiability (SAT) solvers are currently very effective in practice. However, there are still many challenging problems for SAT solvers. Nowadays, extra computational power is no longer coming from higher processor frequencies. At the same time, multicore architectures are becoming predominant. Exploiting this new architecture is essential for the evolution of SAT solvers. Due to the increasing interest in parallel SAT solving, it is important to give an overview of what has been done so far. This paper presents an overview of parallel SAT solving and it is expected to be a valuable document for researchers in this field. This overview covers the main topics of parallel SAT solving, namely, different approaches and a variety of clause sharing strategies. Additionally, an evaluation of multicore SAT solvers is presented, showing the evolution of multicore SAT solvers over the last years.     

SMT求解器理论组合技术研究

可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎.理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景.因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术.通过对照实验,评估...     

Comparing direct and iterative equation solvers in a large structural analysis software system

This paper describes two vectorized implementations of preconditioned conjugate gradient (PCG) solvers. Sparse and diagonal matrix storage schemes are described and compared. A vectorized incomplete Choleski preconditioning is described and compared with Jacobi preconditioning. A modification to the basic no-fill incomplete Choleski method to improve performance and robustness is described. The two PCG solvers are compared with direct Choleski methods using a sparse Choleski solver from SPARSPAK and a vectorized variable-band Choleski solver developed at NASA Langley Research Center. All of the linear equation solvers are implemented in a large structural analysis finite element software system called the Computational Structural Mechanics (CSM) Testbed. The CSM Testbed is used to provide a common software system in which new methods are developed and tested. Several representative two- and three-dimensional structural analysis problems are solved using the various equation solvers. Results are given from runs made on the CONVEX C220 and CRAY 2 computer systems. Comparisons of the convergence rates for the iterative solvers as well as the computation rates, number of operations, and overall CPU time required by all of the equation solvers are given.