Meta-solving

1. Goose
   TL;DR: Goose implements three meta-solving techniques. First, ML-driven algorithm selection based on empirical hardness models for runtime prediction. Second, probabilistic satisfiability inference – an ML approach to determine which subproblems are most likely satisfiable. Finally, time iterative deepening an exponentially increasing wallclock timeout of the ML constructed sequential portfolio.

2. MachSMT
   TL;DR: MachSMT is a tool that uses machine learning to predict the run time of SMT solvers for a given formula, enabling efficient solver selection. Extensive evaluations show it frequently outperforms competition winners and improves solver configurations like cvc5.