ConcurrentSolver

A Solver whose resolution strategy explores the alternatives of a goal's search tree -- matching clauses at a choice point, the branches of a disjunction, the several solutions of a backtracking primitive -- concurrently, as independent Kotlin coroutines, rather than one at a time as :solve-classic/:solve-streams do. Obtained via ConcurrentSolverFactory or, generically, via it.unibo.tuprolog.solve.Solver.concurrent.

Each coroutine models a single it.unibo.tuprolog.solve.concurrent.fsm.State transition (see that package for how a resolution step is represented); whenever a transition has several possible successors, one coroutine is launched per successor, all of them free to run in parallel on whatever dispatcher backs the current platform. As a consequence, the order in which Solutions are produced is not guaranteed to match the left-to-right, depth-first order of standard SLD resolution -- unlike :solve-classic, whose solutions always come out in that deterministic order. Prefer this solver when a goal has independent, parallelizable alternatives worth spreading across CPU cores (e.g. an N-queens-style search with many disjoint branches) and solution order does not matter; prefer :solve-classic (it.unibo.tuprolog.solve.Solver.prolog) when ISO-conformant, deterministic solution ordering is required, or when the overhead of spawning a coroutine per choice point would outweigh the parallelism gained (e.g. goals with few, cheap alternatives).

Concurrency caveat: mutating operations on a it.unibo.tuprolog.solve.MutableSolver built on top of this strategy (e.g. assertZ/retract performed by a primitive while other branches are still running) are not synchronized against one another; concurrently mutating the dynamic knowledge base from multiple branches of the same resolution can race and lose updates. Read-only resolution (the common case) is unaffected, since each branch carries its own immutable ConcurrentExecutionContext.

val solver = ConcurrentSolverFactory.solverWithDefaultBuiltins(staticKb = theory)
val channel = solver.solveConcurrently(goal, SolveOptions.allLazily())
for (solution in channel) {
    println(solution)
}

See also