Incremental Track

The goal of the incremental track established in 2022 is to evaluate the performance and applicability of MaxSAT solvers in applications requiring solving a sequence of related MaxSAT instances.

Motivation

In various types of real-world applications, solving the underlying computational problem requires solving a sequence of incrementally generated optimization problem instances. When cast into MaxSAT, an initial MaxSAT instance is in such scenarios iteratively modified by adding (hard or soft) clauses or changing the weights of soft clauses, between solver invocations. Solver invocations may also be made under different assumptions (i.e., under different forced partial assignments to the variables of the instance).

While it is possible to solve a sequence of related MaxSAT instances independently, i.e. by invoking the solver independently on each instance in the sequence, more efficiency could be obtained by reusing knowledge (e.g. unsatisfiable cores, clauses learned by an internal SAT solver withing the MaxSAT solver, heuristic scores, etc.) between the iterations.

The goal of the incremental track is to provide further incentives for research on incremental MaxSAT solving towards efficiently and truly incremental open-source MaxSAT solvers, to provide incremental MaxSAT benchmark applications for benchmarking incremental solvers, and to provide a uniform interface for incremental MaxSAT solving in order to benefit users who aim to use incremental MaxSAT in applications.

IPAMIR - the Incremental API

Central to the incremental tracks is the now-introduced standard incremental MaxSAT solving interface IPAMIR. The interface extends the already established IPASIR API for incremental SAT [1,2]. The IPAMIR interface consists of 10 functions declared in a C header `ipamir.h`: ipamir_signature, ipamir_init, ipamir_release, ipamir_add_hard, ipamir_add_soft_lit, ipamir_assume, ipamir_solve, ipamir_val_obj, ipamir_val_lit, ipamir_set_terminate

IPAMIR assumes all instances are in so-called normalized form. More specifically, instead of inputting hard and soft clauses separately, applications should input hard clauses (via the ipamir_add_hard function) and declare weighted soft literals (via the ipamir_add_soft_lit function). From a clausal perspective, declaring a literal l soft with weight w corresponds to adding the soft clause (~l) and setting its weight to w. More details of the interface can be found in the comments of the header file.

Solvers may implement any subset of these functions, and benchmarks may make use of any subset of them. That is, you may participate in the incremental track without defining each function. However, the solver must enter state ERROR if the user calls a function which is not supported. For example, if your solver does not support assumptions over literals, after calling ipamir_assume all subsequent ipamir_solve calls must return ERROR. This must be the case also if a sequence of calls is performed in a way that is not supported, e.g., if the user changes the weight of a soft clause by calling ipamir_add_soft_lit after ipamir_solve on an already defined soft literal.

[1] Tomas Balyo, Armin Biere, Markus Iser, and Carsten Sinz. SAT Race 2015. Artificial Intelligence 241:45-65, 2016.

[2] Tomas Balyo and Armin Biere. The Standard Interface for Incremental Satisfiability Solving. https://github.com/biotomas/ipasir.

Incremental Track Benchmarks

(See Call for Benchmarks for submission instructions.) For this newly-established special track on incremental MaxSAT, we strongly encourage the community to support this new development by submitting benchmark applications. In contrast to main track submissions, a benchmark application in the incremental track constitutes a command-line program with a collection of input files. An instance of the benchmark application constitutes an execution of the program which makes multiple MaxSAT solver invocations through the IPAMIR interface on a given input file, the name of which is given as the single command\-line argument to the program.

Your benchmark application must contain a single directory named after the application. Issuing make with the environment variable IPAMIRSOLVER in this directory must result in a successful build of the application using the MaxSAT solver located in ../../maxsat/$(IPAMIRSOLVER) which implements the IPAMIR interface as a static library. Please see the app/ipamirapp directory in the IPAMIR repository for an example application.

Do not hesitate to contact the organizers for help on preparing benchmark applications!

Solver Submissions to the Incremental Track

To submit a solver to the incremental track, implement a subset of functions defined in the IPAMIR header file as described in the comments of the header file. If your solver does not provide support for a particular function, the solver state must be changed to ERROR. Place your solver into a directory named after the solver. Issuing make in this directory must result in a successful build of the solver as a static library. Please see the maxsat/solver2023 directory in the IPAMIR repository for an example (non-incremental) solver. Submit your solver as a single zip or gzipped tar package via email to maxsatevaluation@gmail.com using the subject title "MSE22 solver submission" by May 15 the latest.

Incremental Track Rankings and Correctness

(See also the general rules.) In the incremental track, all solvers will be ranked on each benchmark application independently. For a specific benchmark application, the rank of a solver is determined by the number of solved instances for that benchmark. Solving an instance means that all invocations of the solver are correct, i.e. correctly return either OPTIMUM FOUND or UNSAT as specified in the IPAMIR header.

Following the ideals of the evaluations and taking also into account the fact that the incremental track is now organized for the first time, a solver will not be immediate disqualified if it displays a wrong solution during the execution of the evaluation. The organizers will aim to provide all participants a fair chance of submitting bug fixes. A solver in the incremental track is considered buggy if it does not correctly implement ipamir_solve, ipamir_val_lit or ipamir_val_obj as specified in the IPAMIR header.