Software

• Fix qsoptex Farkas ray
  • Relegate qsoptex to compilation flag

• Make sure the solution match between the two test_solvers

• Check what happens by removing Expand from Formula
  • It can be done only for mps files, since the structure of the formula is not always plain otherwise

• Add inequality support
• Clean up benchmarking suite

• Clean up pydlinear

• Remove unused Config parameters

• Improve nolog options

• Make the sat return type a struct

• Separate smt time between sat and theory

• Sort bounds by value so that it is possible to invalidate just the ones on one side
  • Sorted container for the bounds
  • Find the value of the violated bound for infeasible problems

• Store the value for each bit of the bit iterator and re-use it for next iterations
• Optimise situations where multiple nq constraints are violated at the same time

• Linked variables for bound checking

• Multiple explanations for invalid bounds

• Heuristics options

• In the presence of eq bounds, they should be the only one returned by the active_bounds() method

• Optimal explanation when all nq constraints combination have been explored
• Include a starting iterator when searching lower and upper bounds, so that the search can be resumed from the last point

• Reduce the number of copies of inf and ninf bounds in the bound vector
• Use c++20 format instead of the external library
  • Use Ubuntu 23.04+ for gcc 13+ support

• Return multiple explanations instead of just one when dealing with active constraints

• Improve iterations over nq bounds

• Add symbolic preprocessor for constraints in the form of \(x <> y\)
• Remove completely free variables, especially from nq constraints

• Investigate out of memory

• Handle conflicting constraints in preprocessor

• Fix Invalidly reported constraints in bound processor

• Add support for max and min functions redefinitions

• Update smt2 parser

• Use lazy cache for Formula's GetFreeVariables
• Custom symbolic implementation

• Report need for basis reset in Soplex (a bug in the solver?)

• Use the information from the preprocessor to guide the theory solver. Make sure the graph or causality is respected

• Remove Infinity singleton
• Support string problem input

• Avoid resetting all constraints in the theory solver at each iteration. Instead, reset only the ones that have been removed and add or update the new ones
• NN verification benchmarks

• Add support for integer variables

• Use lower and upper bounds to check for the feasibility of the problem in NN

• Improve theory propagation (simple bounds could imply other bounds, in a chain fashion)
• Improve theory propagation even more

• Add support for LRA

• Use a static array in the Variable class to store the name (and bounds?) of the variable. Use the variable id to access it. The position 0 can be reserved for "dummy".
• Refactor solvers

• Standardize infeasibility explanation

TACAS

• Fix references

• Use american english

• Expand the abstract. Why you'd want to use this tool?

• Start the introduction with the importance of SAT/SMT solvers (and LP?)

• At the end of the introduction add a paragraph on the structure of the paper

• Add a survey of the state of the art SMT solvers

• Move current technical introduction to another section (Preliminaries)
• Artifact evaluation

Future work

• Naive implementation of the rational simplex algorithm for SMT solvers
  • Can it support iterative refinement or precision boosting?

• Specialise symbolic representation for LRA

• Extend cvc5 (or Z3) to use SoPlex as the theory solver

• Investigate over-approximation techniques for neural networks verification