Distributed Solver

The actor solver evaluates a theory across a cluster of actors instead of a single engine. The knowledge base is split among the nodes, each node argues over its own fragment, and the partial results are combined into the final labelling. It is meant for theories large enough that a single solver becomes the bottleneck.

The module is JVM only — it is not published to npm — and is available as the Maven module actor-solver. The cooperative evaluation it implements is described in Pisano, Calegari and Omicini, Multi-agent cooperative argumentation in Arg2P; see References.

This module is more experimental than the rest of the framework. The API described here is the one exercised by its test suite; expect it to change more often than the core engine.

Getting a distributed solver

The entry point is the parallel extension on Arg2pSolver, which yields the libraries of a solver, built as when building a solver by hand:

import it.unibo.tuprolog.argumentation.actor.parallel
import it.unibo.tuprolog.argumentation.core.Arg2pSolver
import it.unibo.tuprolog.argumentation.core.engine.Arg2pPrologSolverFactory
import it.unibo.tuprolog.argumentation.core.runtime.theory.RuleAnnotations

val solver = Arg2pPrologSolverFactory.mutableSolverWithDefaultBuiltins(
    otherLibraries = Arg2pSolver.parallel().to2pLibraries(),
)

parallel(hostname, timeout) takes the host name the node is reached at (127.0.0.1 by default: a cluster spanning several machines needs one the others can reach) and how long solve waits for its answer (60 seconds by default).

Predicates

The module is registered under the identifier parallel and provides:

Predicate	Meaning
`join(Port)`	Starts or joins a cluster on the local machine at the given port (a cluster joined before is left first).
`join(Port, Seed)`	Joins an existing cluster, where `Seed` is the `host:port` of a seed node.
`load`	Sends every clause of the static knowledge base to the cluster.
`solve(Goal, In, Out, Und)`	Evaluates the goal across the cluster, binding the three lists of labelled claims; an error past the timeout.
`reset`	Clears the distributed knowledge base; the evaluations under way end with an error.
`leave`	Leaves the cluster and stops the actor system, freeing its port: the knowledge base stays with the nodes that remain.

A complete session

The order matters: join the cluster, load the theory, query it, then leave.

solver.loadStaticKb(RuleAnnotations.parse(rules, solver.operators))

solver.solve(Struct.parse("join(2551), load")).first()

val answer = solver.solve(Struct.parse("solve(conclusion, In, Out, Und)")).first()
println(answer.substitution)

solver.solve(Struct.parse("leave")).first()

load, reset and solve raise an error when no cluster is joined (before join, or after leave).

Always call leave when you are done. The cluster runs non-daemon threads, and a program that does not leave the cluster may fail to terminate.

Splitting the knowledge base

Nodes receive fragments of the theory according to a splitting principle, and each node evaluates its fragment with its own engine. Because the split is by support relations, conclusions whose arguments span several nodes are resolved by exchanging partial results rather than by rebuilding the whole graph anywhere.