This project provides universal remote control that can be used to control and monitor any solver implementing the Universe interface. This tool may be useful for both solver developers and end-users, as it can be used either for debugging purposes and for finding the most appropriate configuration for solving a particular problems.
The latest release is available here.
RCL is developed using Gradle (at least 7.4.2).
Installing Gradle is not required if you want to build from source (as you can
use the wrapper that is provided in this repository).
To do so, you will need to clone the project:
git clone https://github.com/crillab/remote-control.git
cd remote-control
gradle rclCurrently, the RCL application only supports Java solvers when executed from
the command line, as these solvers are automatically retrieved from the
module path (recall that these solvers must implement the Universe interface,
and provide their implementation of IUniverseSolverFactory).
To execute the application, run the following command after having built RCL
as described above.
It is supposed here that all the jars required by your solver(s) are put in the
my-solvers directory, but you may use another name if you want.
java -p "dist/home:my-solvers" \
-m fr.univartois.cril.rcl/fr.univartois.cril.rcl.RemoteControlSAT, PB or CP Solvers may be considered as black-boxes for laypeople. They often provide many parameters, and understanding the impact of changin one of them is not straightforward. On the contrary, solver developers often know well how to interpret the behavior of their solver, and how to tune it to get the best performance on a hard instance. In both cases, monitoring the behavior of the solver is crucial. The most common approach is to regularly output the solvers statistics in the console in which the solver is run. Another approach is that implemented in Sat4j, which provides a remote control to modify its configuration and to graphically visualize the statistics of the search. Based on the Universe interface, this repository provides a universal remote control inspired by that of Sat4j, that can be used to control and monitor any solver implementing the Universe interface. This tool may be useful for both solver developers and end-users, as it can be used either for debugging purposes and for finding the most appropriate configuration for solving a particular problem.
The remote control provides a graphical interface for configuring the solver
by exploiting the methods provided by the IUniverseConfigurableSolver.
The user interface is dynamically built based on the strategies that are
recognized by the solver for variable and value selection heuristics, restart
policies and learned constraint deletions (a different tab is provided for each
of these features, see Figure\ \ref{fig:mainmenu}).
The user can choose the strategy he wants to apply by selecting it in a
combobox, and he can then set the (optional) parameters of the selected strategy
to finely configure it.
The critical feature of the remote control is that this configuration can be
applied before running the solvers, but also while it is running (of course,
if the underlying solver supports such an update).
This allows one to immediately see the impact of a strategy compared to another,
and thus to guide the user towards finding the most appropriate one to solve his
problem.
In the same spirit, the remote control allows one to manually trigger a restart
or a learned constraint deletion.
For solvers that do not implement IUniverseConfigurableSolver, the remote
control can still be used, but the configuration tabs are disabled.
Only the solver execution and its monitoring are available for such solvers.
As for the remote control provided by Sat4j, the solver's statistics are displayed live during its execution. In addition to the solver's logs that are redirected to the remote control window, six plots are updated at each conflict encountered by the solver, as shown in Figure\ \ref{fig:rclplot}:
- the size of the constraint learned by the solver after this conflict,
- the quality of the learned constraints,
- the number of negative (resp. positive) decisions made before the conflict,
- the decision level at which the conflict occured, and
- the total number of assigned variables when the conflict occured.
Together, these plots provide a representation of the solver behavior that is more visual and interpretable than their textual counterpart printed in the logs.
The remote control also offers to display the search tree while it is being explored by the solver. Each time a new decision is made by the solver, a node is added to the tree, with a label displaying the corresponding decision. Conflicts and solutions are the leaves of the tree, and are displayed in red and green, respectively. An example of such a tree is given on Figure\ \ref{fig:tree}. This feature should however be used with caution, and on rather small inputs. Indeed, the search tree that is built by the solver may be very large, and displaying it may not be possible in the window of the remote control. Additionally, showing the search tree live may have an impact on the solver performance, which may become very slow.
