SAPS Tuning

SAPS is a SAT solver with four independent parameters. Correcly choosing those parameters depending on your SAT instances can greatly reduce runtime.

The implementation we tune in this example is the one shipped with UBCSAT version 1.1.0, available at UBCSAT homepage. As we tune for penalized runtime, have simple parameters, and UBCSAT can be called from console, it is possible to use the out-of-the-box tuning provided by OPTANO Algorithm Tuner. The parameters for that would be:

--master --maxParellelEvaluations=8 --basicCommand="[PATH]\ubcsat.exe -alg saps -i {instance} {arguments} -timeout 10 -cutoff max -seed 42" --trainingInstanceFolder=[PATH] --parameterTree=[PATH]\sapsParameterTree.xml

However, customizing OPTANO Algorithm Tuner reduces overhead and comes with increased precision. For applications dealing with small SAT instances solvable in milliseconds, this can make a noticeable difference.

Please consider the technical preparations before using OPTANO Algorithm SAPS Tuner.

Moreover note, that you may use FuzzSAT as a generator for your SAT instances.

Overview

The solution implementing OPTANO Algorithm SAPS Tuner consists of the classes

  • Program.cs
  • SapsUtils.cs,
  • SapsRunner.cs,
  • SapsRunnerConfiguration.cs,
  • SapsRunnerConfigurationParser.cs,
  • SapsRunnerFactory.cs,
  • GenericSapsEntryPoint.cs, and
  • GenericParameterization.cs.

Program.cs is responsible for reading in parameters and starting OPTANO Algorithm Tuner.
SapsUtils.cs is responsible for reading in instances and building the parameter tree.
SapsRunner.cs starts parameter evaluations, i.e. single SAPS runs.
SapsRunnerConfiguration.cs wraps the configuration and the configuration builder of the SAPS Tuner.
SapsRunnerConfigurationParser.cs defines custom arguments for SAPS tuning and modifies the output of --help accordingly.
SapsRunnerFactory.cs builds SapsRunner instances using a given parameter combination.
GenericSapsEntryPoint.cs provides a generic entry point for different SAPS runner parametrizations.
GenericParameterization.cs defines the different generic parameterization options.

Customization

The SAPS tuning classes are a simple example on how to customize OPTANO Algorithm Tuner to your liking.

As UBCSAT takes a file name as input, we don't need our own IInstance implementation, but can use the InstanceSeedFile provided by OPTANO Algorithm Tuner. Likewise, the target function of penalized runtime tuning is already implemented by SortByRuntime, and the relevant result by RuntimeResult. This leaves us to implement ITargetAlgorithm and ITargetAlgorithmFactory, which are implemented in SapsRunner respectively SapsRunnerFactory. Additionally, we have to take care of parsing the SAPS Tuner specific parameters in the SapsRunnerConfigurationParser and create the respective SapsRunnerConfiguration.

The complete call to the tuner is built in Program.cs.

Parameter

For parsing the parameters, a SapsRunnerConfigurationParser is implemented which parses the specific parameters from the command line, extracts the ones that refer to the SAPS runner configuration and passes the remaining arguments to the OPTANO Algorithm Tuner.

The Main method shows how to call the tuner code from your customized application.

Specific Parameters

OPTANO Algorithm SAPS Tuner checks for the following additional parameters:

--master
Indicates that this instance of the application should act as master.
--executable={PATH}
The path to the ubcsat executable.
--genericParametrization=Optano.Algorithm.Tuner.Saps.CustomModel.GenericParameterization
Specifies the generic parameterization to use for the genetic enginering model. Must be a member of the Optano.Algorithm.Tuner.Saps.CustomModel.GenericParameterization enum. Valid Values are:
Default
RandomForestReuseOldTrees
RandomForestAverageRank
StandardRandomForest (same as Default)
--factorParK={VALUE} [0]
The factor for the penalization of the average runtime. Needs to be greater or equal to 0. If 0, OAT sorts first by highest number of uncancelled runs and then by unpenalized average runtime.
--rngSeed={VALUE} [42]
The random number generator seed, which generates #numberOfSeeds seeds for every instance of the SAPS algorithm.
--numberOfSeeds={VALUE} [1]
Specifies the number of seeds, which are used for every instance of the SAPS algorithm. Needs to be greater than 0.

The SapsRunnerConfigurationParser

SapsRunnerConfigurationParser.cs defines the class SapsRunnerConfigurationParser which parses specific parameters from the command line and extracts the ones that should be handled by OPTANO Algorithm Tuner. Additionally, it defines a useful output if the help parameter is provided.

SapsRunnerConfigurationParser extends HelpSupportingArgumentParser provided by OPTANO Algorithm Tuner and consists of

  • fields and properties for the arguments to read
  • the methods CreatePreprocessingOptionSet and CreateMasterOptionSet which define the possible options and how to parse them. The descriptions of those will be printed when help is requested.
  • the method PrintHelp which prints both the custom options and the ones defined by OPTANO Algorithm Tuner.
  • the method ParseArguments which takes care of the order and dependencies between parsing of parameters, and also throws exceptions in case that some required parameters are not set.

A Closer Look on SapsRunner

SapsRunner is the class that starts SAPS runs for certain parameter combinations. Every instance of SapsRunner is used for several evaluations on the same parameter combination. Therefore, the parameters are set in the constructor, while the instance for the run is specified in a method call.

OPTANO Algorithm SAPS Tuner handles its task by starting UBCSAT in an additional process, waiting for it and reading the process output. Note that Run(InstanceSeedFile instance, CancellationToken cancellationToken) has to take care of the provided cancellation token. SapsRunner handles this by registering a ProcessUtils.CancelProcess(process) method. This method is part of OPTANO Algorithm Tuner and can therefore also be used by your own implementations.

If you want to handle cancelled evaluations as results with an IsCancelled flag set to true, you have to make sure to call cancellationToken.ThrowIfCancellationRequested() in case of a cancellation. SapsRunner does just that.

Error Handling

To handle upcoming errors (e.g. crash of target algorithm) reasonable, the method CreateRuntimeResult() is implemented in SapsRunner. This method reads out the console output and checks for "CPUTime_Median =". If not present, it creates a cancelled result and sets the corresponding runtime to the given timeout.

How to Use

The command to run OPTANO Algorithm SAPS Tuner may look like

dotnet Optano.Algorithm.Tuner.Saps.dll --master --maxParallelEvaluations=4 --trainingInstanceFolder=[PATH] --cpuTimeout=10 --executable=[PATH]

For starting a worker you have to supply the master host name and the port:

dotnet Optano.Algorithm.Tuner.Saps.dll --seedHostName=[HOSTNAME] --port=[PORT]

The master will print the required information on startup.

Troubleshooting:

If the worker does not connect to the master, try to explicitely set the IP adress of the master as host name with --ownHostName=[IPADRESS] by starting the master.

Unittests

For details about the unittests of OPTANO Algorithm SAPS Tuner please see Unittests.