isla
isla copied to clipboard
[FEATURE] Replace queue/cost function solver approach by coverage-guided random choice + backtracking
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.