Next: Introduction, Previous: (dir), Up: (dir) [Contents][Index]
This is the cl-maxsat Reference Manual, version 0.1, generated automatically by Declt version 3.0 "Montgomery Scott" on Fri Jun 26 10:22:23 2020 GMT+0.
| • Introduction | What cl-maxsat is all about | |
| • Systems | The systems documentation | |
| • Modules | The modules documentation | |
| • Files | The files documentation | |
| • Packages | The packages documentation | |
| • Definitions | The symbols documentation | |
| • Indexes | Concepts, functions, variables and data types |
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>)...).
Example:
(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.
When solver-designator argument is :maxsat-competition, solve function accepts :year :track :name arguments
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.
:complete
:LMHS --- requires CPLEX:MaxHS --- requires CPLEX:Open-WBO:maxino:QMaxSAT:QMaxSATuc:incomplete
:LMHS-inc --- requires CPLEX:MaxHS-inc --- requires CPLEX:Open-WBO-LSUThis library is at least tested on implementation listed below:
Also, it depends on the following libraries:
cl-sat :
trivia by Masataro Asai : NON-optimized pattern matcher compatible with OPTIMA, with extensible optimizer interface and clean codebase
alexandria by Nikodemus Siivola nikodemus@sb-studio.net, and others. : Alexandria is a collection of portable public domain utilities.
iterate by ** : Jonathan Amsterdam's iterator/gatherer/accumulator facility
Licensed under LGPL v3.
Copyright (c) 2019 Masataro Asai (guicho2.71828@gmail.com) Copyright (c) 2019 IBM Corporation
Next: Modules, Previous: Introduction, Up: Top [Contents][Index]
The main system appears first, followed by any subsystem dependency.
| • The cl-maxsat system |
Masataro Asai
LGPL
Common Lisp API to MAX-SAT Solvers
0.1
cl-maxsat.asd (file)
src (module)
Modules are listed depth-first from the system components tree.
| • The cl-maxsat/src module |
cl-maxsat (system)
src/
Files are sorted by type and then listed depth-first from the systems components trees.
| • Lisp files |
| • The cl-maxsat.asd file | ||
| • The cl-maxsat/src/0-package.lisp file | ||
| • The cl-maxsat/src/2-class.lisp file | ||
| • The cl-maxsat/src/3-dimacs.lisp file | ||
| • The cl-maxsat/src/4-competition.lisp file |
Next: The cl-maxsat/src/0-package․lisp file, Previous: Lisp files, Up: Lisp files [Contents][Index]
cl-maxsat.asd
cl-maxsat (system)
Next: The cl-maxsat/src/2-class․lisp file, Previous: The cl-maxsat․asd file, Up: Lisp files [Contents][Index]
Next: The cl-maxsat/src/3-dimacs․lisp file, Previous: The cl-maxsat/src/0-package․lisp file, Up: Lisp files [Contents][Index]
src (module)
src/2-class.lisp
Next: The cl-maxsat/src/4-competition․lisp file, Previous: The cl-maxsat/src/2-class․lisp file, Up: Lisp files [Contents][Index]
src (module)
src/3-dimacs.lisp
Previous: The cl-maxsat/src/3-dimacs․lisp file, Up: Lisp files [Contents][Index]
src (module)
src/4-competition.lisp
Next: Definitions, Previous: Files, Up: Top [Contents][Index]
Packages are listed by definition order.
| • The cl-maxsat package |
0-package.lisp (file)
Definitions are sorted by export status, category, package, and then by lexicographic order.
| • Exported definitions | ||
| • Internal definitions |
Next: Internal definitions, Previous: Definitions, Up: Definitions [Contents][Index]
| • Exported functions | ||
| • Exported generic functions | ||
| • Exported classes |
Next: Exported generic functions, Previous: Exported definitions, Up: Exported definitions [Contents][Index]
3-dimacs.lisp (file)
3-dimacs.lisp (file)
Next: Exported classes, Previous: Exported functions, Up: Exported definitions [Contents][Index]
automatically generated reader method
2-class.lisp (file)
Previous: Exported generic functions, Up: Exported definitions [Contents][Index]
2-class.lisp (file)
sat-instance (class)
:soft-clauses
soft-clauses (generic function)
Previous: Exported definitions, Up: Definitions [Contents][Index]
| • Internal special variables | ||
| • Internal functions | ||
| • Internal generic functions | ||
| • Internal conditions |
Next: Internal functions, Previous: Internal definitions, Up: Internal definitions [Contents][Index]
4-competition.lisp (file)
Next: Internal generic functions, Previous: Internal special variables, Up: Internal definitions [Contents][Index]
returns a status code, signal errors for non-0 return code
4-competition.lisp (file)
returns a status code, ignores error status
4-competition.lisp (file)
returns a string, ignores error status.
This is only for the ’light’ routines as the process may not be terminated properly.
4-competition.lisp (file)
returns a string, signal errors for non-0 return code.
This is only for the ’light’ routines as the process may not be terminated properly.
4-competition.lisp (file)
4-competition.lisp (file)
4-competition.lisp (file)
4-competition.lisp (file)
Next: Internal conditions, Previous: Internal functions, Up: Internal definitions [Contents][Index]
Returns function
4-competition.lisp (file)
Previous: Internal generic functions, Up: Internal definitions [Contents][Index]
4-competition.lisp (file)
competition-setup-error (condition)
4-competition.lisp (file)
competition-setup-error (condition)
4-competition.lisp (file)
error (condition)
print-object (method)
:year
:track
:name
4-competition.lisp (file)
competition-setup-error (condition)
4-competition.lisp (file)
error (condition)
4-competition.lisp (file)
competition-setup-error (condition)
Previous: Definitions, Up: Top [Contents][Index]
| • Concept index | ||
| • Function index | ||
| • Variable index | ||
| • Data type index |
Next: Function index, Previous: Indexes, Up: Indexes [Contents][Index]
| Jump to: | C F L M |
|---|
| Jump to: | C F L M |
|---|
Next: Variable index, Previous: Concept index, Up: Indexes [Contents][Index]
| Jump to: | C D F G M P R S |
|---|
| Jump to: | C D F G M P R S |
|---|
Next: Data type index, Previous: Function index, Up: Indexes [Contents][Index]
| Jump to: | *
N S T Y |
|---|
| Jump to: | *
N S T Y |
|---|
Previous: Variable index, Up: Indexes [Contents][Index]
| Jump to: | B C D M N P S U |
|---|
| Jump to: | B C D M N P S U |
|---|