The queue-based approach with the highly problem-specific cost function is a central pain point in the ISLa solver. It might be the most significant performance barrier in ISLa. The old solver strategy should be replaced by an approach which
chooses random expansions/solutions, only considering syntactic (k-paths?) and semantic (?) coverage criteria
backtracks whenever no solution is found for a given sequence of random choices (e.g., the left element of a disjunction, a particular k-path expansion, etc.).
The state of the resulting solver will be much smaller, maintaining the alternatives chosen so far to support coverage guidance and backtracking. Furthermore, the solver will be nondeterministic (for different random seeds) compared to the ISLa 1.x solver.
The queue-based approach with the highly problem-specific cost function is a central pain point in the ISLa solver. It might be the most significant performance barrier in ISLa. The old solver strategy should be replaced by an approach which
The state of the resulting solver will be much smaller, maintaining the alternatives chosen so far to support coverage guidance and backtracking. Furthermore, the solver will be nondeterministic (for different random seeds) compared to the ISLa 1.x solver.