A computer-implemented method for solving a satisfiability (SAT) problem includes defining a formula, including variables, which refers to properties of a target system. Using a chosen search strategy, a search process is performed over possible value assignments of the variables for a satisfying assignment that satisfies the formula. A performance metric estimating an effectiveness of the search process is periodically evaluated during the search process. The strategy of the search process is modified responsively to the evaluated performance metric. The method determines, using the search process, whether the formula is satisfiable on the target system.