Унапређивање SMT решаваче коришћењем CSP техника и техника паралелизације

Abstract

SMT решавачи имплементирају процедуре одлучивања за испитивање задовољивости логичких формула првог реда у односу на неку унапред задату одлучиву теорију. Ослањајући се на моћне технике за решавање проблема исказне задовољивости (SAT)у комбинацији са специфичним процедурама одлучивања које омогућавају резоновање у конкретној теорији. Типична примена SMT решавача је у верификацији софтвера, па су зато теорије које се стандарно користе у SMT решавачима прилагођене тој врсти примене ...

SMT solvers implement decision procedures that check for satisfiability of first-order logical formulae with respect to some decidable theory. They rely on the powerful techniques that are used for solving boolean satisfiability problem (SAT), combined with specific procedures that permit reasoning in a particular theory. Typical applications of SMT solvers are mostly found in software verification, and for this reason the theories frequently considered in SMT solvers are best suited for such kind of applications. Extending the applicability of SMT solvers to other areas may require defining new SMT theories, as well as developing the corresponding decision procedures for such theories. In that sense, in this thesis we consider improving of SMT solvers by extending their applicability to solving CSP problems. Such problems consider variables with finite domains, and the goal is to find the assignment of values to the variables of the problem satisfying all the imposed constraints. When CSP solving is considered, the main drawback of the existing SMT theories is that they are not adapted to the problems with finite domains, and are also incapable of reasoning about global constraints, which play the significant role in most CSP problems. For this reason, in this thesis a novel SMT theory is defined that enables natural representation of CSP problems, since it includes support for some frequently used global constraints. For such theory, we developed a decision procedure based on the existing techniques borrowed from the traditional CSP solvers, but these techniques are adapted in the way that permits their usage within SMT solvers. The decision procedure currently supports two types of global constraints: the alldifferent constraint and the linear constraint. In case of the alldifferent constraint, the main contribution is a novel algorithm for generating explanations of conflicts and propagations, which is required for the conflict analysis. In case of the linear constraint, a novel filtering algorithm is developed that takes into consideration the existence of the alldifferent constraints in the given problem, which can lead to a stronger propagation. Another direction of improving SMT solvers that is considered in the thesis is the usage of the parallelization techniques. We consider the parallelization of the simplex algorithm, which is used in SMT solvers as the decision procedure for the linear arithmetic. We also consider the parallel portfolio approach, as well as the hybridization of the two approaches. A comprehensive experimental evaluation is provided on a large number of instances, both industrial and randomly generated. For the purpose of all the mentioned research, during the work on the thesis a new open-source SMT solver called argosmt is developed, based on DPLL(T ) architecture.