Feature Extraction from an SMT Problem

One way of solving complex satisfiability problems is by using the method of SMT(Satisfiability Modulo Theories). For satisfiability problems that are harder to solve than trivial ones, we could very well save ourselves a lot of time if we choose the most suitable solver immediately. These problems tend to take some time to solve, in accordance to their complexities, and different solvers specialise in different types of satisfiability problems. SMT is similar to the SAT modeling language but it is at a higher level, and allows further abstraction by including theories. In comparison to SAT problems, SMTproblems are more information-dense. In addition, SMT solvers often come with complementary performance profiles. In this paper we entertain the idea that we could indeed find a similarity between problems by collecting metadata from them. As a result of this, a feature extractor to count a manually defined set of features over SMT-LIB problems has been implemented. The idea is that if we have a problem, then these characteristics, if chosen carefully, could help us recognise problems with similar feature counts that has already been successfully solved within a portfolio solver system. The most successful solver for those problems may then be the most suitable solver for our problem as well, or at least we can use similar solving methods. Examples of these features are the number of uses of certain functions, or the total number of symbols.These test runs have in addition to collecting the metadata shown some variation between the benchmark groups whose results are presented and analysed grouped bylogics in the result section of this paper