Common Lisp API to MAX-SAT Solvers
Cl-Maxsat - Common Interface to MAX-SAT Solvers from Common Lisp
The API extends the
SOLVE generic function in CL-SAT.
The format for denoting the logic formula is equivalent.
The extension allows
SOLVE function to take an additional
:soft-clauses keyword argument,
which is a list of form
((<weight> <logical form>)...).
(solve '(and (or a b) (or (not e) d) (or (not d) c)) :maxsat-competition :soft-clauses '((1 (and d c)) (2 (and b (not e)))) :year 2017 :track :complete :name :maxhs)
Similar to CL-SAT, this library supports various competition winners from the previous MaxSAT competitions.
solver-designator argument is
solve function accepts
and try to download and build the specified solver if it was not done before.
The zip-compressed source codes distributed at the competition sites do not follow the consistent build procedure unlike SAT competitions. Some fails to compile on the newer GCC (e.g. those in Ubuntu 18.04). However, we patch up the build scripts so that they build successfully.
Note that a couple of solvers require MILP solvers and the patches are hard-coding that we will use IBM CPLEX. CPLEX binary should be visible in the PATH when using those solvers. However, not all solvers rely on CPLEX, and also some solvers allow switching between CPLEX and other solvers (e.g. Gurobi, Xpress). If there are such needs we may support them.
- MaxSAT Evaluation 2017
:LMHS--- requires CPLEX
:MaxHS--- requires CPLEX
:LMHS-inc--- requires CPLEX
:MaxHS-inc--- requires CPLEX
- MaxSAT Evaluation 2018
- not supported yet
This library is at least tested on implementation listed below:
- SBCL 1.4.10 on X86-64 Linux 4.15.0-43-generic (author's environment)
Also, it depends on the following libraries:
trivia by Masataro Asai : NON-optimized pattern matcher compatible with OPTIMA, with extensible optimizer interface and clean codebase
alexandria by Nikodemus Siivola firstname.lastname@example.org, and others. : Alexandria is a collection of portable public domain utilities.
iterate by ** : Jonathan Amsterdam's iterator/gatherer/accumulator facility
Author, License, Copyright
Licensed under LGPL v3.
Copyright (c) 2019 Masataro Asai (email@example.com) Copyright (c) 2019 IBM Corporation