This course aims at the design, implementation, and optimization of an SMT-compliant theory solver using the Simplex algorithm.

Linear arithmetic

We consider the theory over the reals with addition, which we call linear arithmetic. Theory constraints are of the form a₀x₀+a₁x₁+…+a_nx_n~b where the x_i are real-valued variables, the a_i and b are rational numbers, + is the commonly known arithmetic plus operator, and ~ is one of the binary relations <, ≤, =, ≥, and >.  The satisfiability problem for linear arithmetic poses the question whether a set of linear arithmetic constraints have a common satisfying solution.

Simplex

The Simplex algorithm was originally designed for solving optimization problems, specified by a set of linear arithmetic constraints and an objective function. A solution to such a linear program is a solution to the constraints which gives a maximal (resp. minimal) value for the objective function. In a first phase, Simplex searches for a initial solution satisfying the constraints. This initial solution is iteratively improved in the second phase to determine a solution which maximizes (resp. minimizes) the value of the objective function. We are interested in solving the satisfiability problem for linear arithmetic, hence we will use the first phase of Simplex only.

First-order logic over linear arithmetic

We consider the existential fragment of first-order logic over linear arithmetic. Formulas in this logic are Boolean combinations of linear arithmetic constraints. For example, x + 2 * y ≥ 0 and (x < 0 or 2 * x + 4 * y + 2 < 0) is a formula in this logic, which is satisfiable (e.g., the assignment x=-1 and y=0.5 satisfies it). We obtain the Boolean skeleton of such a formula by replacing each theory constraint by an auxiliary Boolean variable, e.g., A and (B or C) is a Boolean skeleton of our example formula.

SMT solving

SAT solver can decide whether a propositional logic formula is satisfiable, that is they check the existence of an assignment of the Boolean variables to True or False such that the formula is satisfied. SAT modulo theories (SMT) solving aims at checking satisfiability of existential fragments of first-order-logic formulas over different theories. In this course we consider SMT solving for the Boolean combination of linear arithmetic constraints.

While the SAT-solver tries to construct a satisfying assignment for the Boolean skeleton of the SMT formula iteratively, the theory solver verifies the conjunction of the constraints which have to hold according to the so far constructed assignment. For our example formula, the SAT solver could assign True to A and send the constraint x + 2 * y ≥ 0 to the theory solver, which detects satisfiability. After assigning True also to B and C the theory solver will report unsatisfiability and give back x + 2 * y ≥ 0 and 2 * x + 4 * y + 2 < 0 as reason. The SAT solver uses this information to undo a part of the current assignment (backtrack), learn that it should not assign both A and C to True, and continue the search.

1. Incrementality: The theory solver should be able to accept theory constraints one after the other. It should have a method to check the constraints received so far for consistency. For efficiency it is important that the solver makes use of the result of earlier checks.
2. Minimal infeasible subset generation: If the theory solver detects a conflict, it should give a reason for the unsatisfiability. The usual way is to determine an unsatisfiable subset of the constraints which is ideally minimal in the sense that if we remove a constraint the remaining ones become satisfiable.
3. Backtracking: The solver should be able to backtrack, i.e., remove previously added constraints.

Tasks of the practical course

The participants will design and implement a theory solver for linear arithmetic fulfilling the abovementioned properties. The theory solver will be implemented in C++ and embedded into the open source SMT solver OpenSMT. We will optimize the performance of the theory solver, which requires a thoughtfully designed data structure and the development of smart heuristics. Hence, the design phase in the beginning needs the thorough awareness of the functionality and recent developments of the Simplex algorithm.

Course dates

The course dates will be announced soon. All necessary materials and information will be announced in the learning room L2P.

Prerequisites

Contact