The cl-maxsat Reference Manual

Table of Contents

Next: , Previous: , Up: (dir)   [Contents][Index]

The cl-maxsat Reference Manual

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.


Next: , Previous: , Up: Top   [Contents][Index]

1 Introduction

Cl-Maxsat - Common Interface to MAX-SAT Solvers from Common Lisp

Usage

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)

Available solvers

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.

Dependencies

This library is at least tested on implementation listed below:

Also, it depends on the following libraries:

Installation

Author, License, Copyright

Licensed under LGPL v3.

Copyright (c) 2019 Masataro Asai (guicho2.71828@gmail.com) Copyright (c) 2019 IBM Corporation


Next: , Previous: , Up: Top   [Contents][Index]

2 Systems

The main system appears first, followed by any subsystem dependency.


Previous: , Up: Systems   [Contents][Index]

2.1 cl-maxsat

Author

Masataro Asai

Contact

guicho2.71828@gmail.com

License

LGPL

Description

Common Lisp API to MAX-SAT Solvers

Version

0.1

Dependencies
Source

cl-maxsat.asd (file)

Component

src (module)


Next: , Previous: , Up: Top   [Contents][Index]

3 Modules

Modules are listed depth-first from the system components tree.


Previous: , Up: Modules   [Contents][Index]

3.1 cl-maxsat/src

Parent

cl-maxsat (system)

Location

src/

Components

Next: , Previous: , Up: Top   [Contents][Index]

4 Files

Files are sorted by type and then listed depth-first from the systems components trees.


Previous: , Up: Files   [Contents][Index]

4.1 Lisp


Next: , Previous: , Up: Lisp files   [Contents][Index]

4.1.1 cl-maxsat.asd

Location

cl-maxsat.asd

Systems

cl-maxsat (system)


Next: , Previous: , Up: Lisp files   [Contents][Index]

4.1.2 cl-maxsat/src/0-package.lisp

Parent

src (module)

Location

src/0-package.lisp

Packages

cl-maxsat


Next: , Previous: , Up: Lisp files   [Contents][Index]

4.1.3 cl-maxsat/src/2-class.lisp

Parent

src (module)

Location

src/2-class.lisp

Exported Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

4.1.4 cl-maxsat/src/3-dimacs.lisp

Parent

src (module)

Location

src/3-dimacs.lisp

Exported Definitions

Previous: , Up: Lisp files   [Contents][Index]

4.1.5 cl-maxsat/src/4-competition.lisp

Parent

src (module)

Location

src/4-competition.lisp

Internal Definitions

Next: , Previous: , Up: Top   [Contents][Index]

5 Packages

Packages are listed by definition order.


Previous: , Up: Packages   [Contents][Index]

5.1 cl-maxsat

Source

0-package.lisp (file)

Use List
Exported Definitions
Internal Definitions

Next: , Previous: , Up: Top   [Contents][Index]

6 Definitions

Definitions are sorted by export status, category, package, and then by lexicographic order.


Next: , Previous: , Up: Definitions   [Contents][Index]

6.1 Exported definitions


Next: , Previous: , Up: Exported definitions   [Contents][Index]

6.1.1 Functions

Function: parse-wdimacs-output FILE INSTANCE
Package

cl-maxsat

Source

3-dimacs.lisp (file)

Function: print-wcnf INSTANCE &optional STREAM *VERBOSITY*
Package

cl-maxsat

Source

3-dimacs.lisp (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

6.1.2 Generic functions

Generic Function: soft-clauses OBJECT
Package

cl-maxsat

Methods
Method: soft-clauses (MAXSAT-INSTANCE maxsat-instance)

automatically generated reader method

Source

2-class.lisp (file)


Previous: , Up: Exported definitions   [Contents][Index]

6.1.3 Classes

Class: maxsat-instance ()
Package

cl-maxsat

Source

2-class.lisp (file)

Direct superclasses

sat-instance (class)

Direct methods
  • variables (method)
  • solve (method)
  • initialize-instance (method)
  • soft-clauses (method)
Direct slots
Slot: soft-clauses
Initargs

:soft-clauses

Readers

soft-clauses (generic function)


Previous: , Up: Definitions   [Contents][Index]

6.2 Internal definitions


Next: , Previous: , Up: Internal definitions   [Contents][Index]

6.2.1 Special variables

Special Variable: *base-url*
Package

cl-maxsat

Source

4-competition.lisp (file)


Next: , Previous: , Up: Internal definitions   [Contents][Index]

6.2.2 Functions

Function: cmd COMMAND &rest FORMAT-ARGS

returns a status code, signal errors for non-0 return code

Package

cl-maxsat

Source

4-competition.lisp (file)

Function: cmd* COMMAND &rest FORMAT-ARGS

returns a status code, ignores error status

Package

cl-maxsat

Source

4-competition.lisp (file)

Function: cmd*/s COMMAND &rest FORMAT-ARGS

returns a string, ignores error status.
This is only for the ’light’ routines as the process may not be terminated properly.

Package

cl-maxsat

Source

4-competition.lisp (file)

Function: cmd/s COMMAND &rest FORMAT-ARGS

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.

Package

cl-maxsat

Source

4-competition.lisp (file)

Function: detect-cplex ()
Package

cl-maxsat

Source

4-competition.lisp (file)

Function: download-and-extract YEAR TRACK NAME
Package

cl-maxsat

Source

4-competition.lisp (file)

Function: rel DIRECTORY
Package

cl-maxsat

Source

4-competition.lisp (file)


Next: , Previous: , Up: Internal definitions   [Contents][Index]

6.2.3 Generic functions

Generic Function: download-and-run-solver YEAR TRACK NAME INPUT DIR RESULT

Returns function

Package

cl-maxsat

Source

4-competition.lisp (file)

Methods
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql incomplete)) (NAME (eql maxhs-inc)) INPUT DIR RESULT
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql incomplete)) (NAME (eql lmhs-inc)) INPUT DIR RESULT
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql incomplete)) (NAME (eql open-wbo-lsu)) INPUT DIR RESULT
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql complete)) (NAME (eql qmaxsatuc)) INPUT DIR RESULT
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql complete)) (NAME (eql qmaxsat)) INPUT DIR RESULT
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql complete)) (NAME (eql maxino)) INPUT DIR RESULT
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql complete)) (NAME (eql open-wbo)) INPUT DIR RESULT
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql complete)) (NAME (eql maxhs)) INPUT DIR RESULT
Method: download-and-run-solver (YEAR (eql 2017)) (TRACK (eql complete)) (NAME (eql lmhs)) INPUT DIR RESULT

Previous: , Up: Internal definitions   [Contents][Index]

6.2.4 Conditions

Condition: build-error ()
Package

cl-maxsat

Source

4-competition.lisp (file)

Direct superclasses

competition-setup-error (condition)

Condition: chmod-error ()
Package

cl-maxsat

Source

4-competition.lisp (file)

Direct superclasses

competition-setup-error (condition)

Condition: competition-setup-error ()
Package

cl-maxsat

Source

4-competition.lisp (file)

Direct superclasses

error (condition)

Direct subclasses
Direct methods

print-object (method)

Direct slots
Slot: year
Initargs

:year

Slot: track
Initargs

:track

Slot: name
Initargs

:name

Condition: download-error ()
Package

cl-maxsat

Source

4-competition.lisp (file)

Direct superclasses

competition-setup-error (condition)

Condition: no-cplex-error ()
Package

cl-maxsat

Source

4-competition.lisp (file)

Direct superclasses

error (condition)

Condition: unzip-error ()
Package

cl-maxsat

Source

4-competition.lisp (file)

Direct superclasses

competition-setup-error (condition)


Previous: , Up: Top   [Contents][Index]

Appendix A Indexes


Next: , Previous: , Up: Indexes   [Contents][Index]

A.1 Concepts

Jump to:   C   F   L   M  
Index Entry  Section

C
cl-maxsat.asd: The cl-maxsat․asd file
cl-maxsat/src: The cl-maxsat/src module
cl-maxsat/src/0-package.lisp: The cl-maxsat/src/0-package․lisp file
cl-maxsat/src/2-class.lisp: The cl-maxsat/src/2-class․lisp file
cl-maxsat/src/3-dimacs.lisp: The cl-maxsat/src/3-dimacs․lisp file
cl-maxsat/src/4-competition.lisp: The cl-maxsat/src/4-competition․lisp file

F
File, Lisp, cl-maxsat.asd: The cl-maxsat․asd file
File, Lisp, cl-maxsat/src/0-package.lisp: The cl-maxsat/src/0-package․lisp file
File, Lisp, cl-maxsat/src/2-class.lisp: The cl-maxsat/src/2-class․lisp file
File, Lisp, cl-maxsat/src/3-dimacs.lisp: The cl-maxsat/src/3-dimacs․lisp file
File, Lisp, cl-maxsat/src/4-competition.lisp: The cl-maxsat/src/4-competition․lisp file

L
Lisp File, cl-maxsat.asd: The cl-maxsat․asd file
Lisp File, cl-maxsat/src/0-package.lisp: The cl-maxsat/src/0-package․lisp file
Lisp File, cl-maxsat/src/2-class.lisp: The cl-maxsat/src/2-class․lisp file
Lisp File, cl-maxsat/src/3-dimacs.lisp: The cl-maxsat/src/3-dimacs․lisp file
Lisp File, cl-maxsat/src/4-competition.lisp: The cl-maxsat/src/4-competition․lisp file

M
Module, cl-maxsat/src: The cl-maxsat/src module

Jump to:   C   F   L   M  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.2 Functions

Jump to:   C   D   F   G   M   P   R   S  
Index Entry  Section

C
cmd: Internal functions
cmd*: Internal functions
cmd*/s: Internal functions
cmd/s: Internal functions

D
detect-cplex: Internal functions
download-and-extract: Internal functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions
download-and-run-solver: Internal generic functions

F
Function, cmd: Internal functions
Function, cmd*: Internal functions
Function, cmd*/s: Internal functions
Function, cmd/s: Internal functions
Function, detect-cplex: Internal functions
Function, download-and-extract: Internal functions
Function, parse-wdimacs-output: Exported functions
Function, print-wcnf: Exported functions
Function, rel: Internal functions

G
Generic Function, download-and-run-solver: Internal generic functions
Generic Function, soft-clauses: Exported generic functions

M
Method, download-and-run-solver: Internal generic functions
Method, download-and-run-solver: Internal generic functions
Method, download-and-run-solver: Internal generic functions
Method, download-and-run-solver: Internal generic functions
Method, download-and-run-solver: Internal generic functions
Method, download-and-run-solver: Internal generic functions
Method, download-and-run-solver: Internal generic functions
Method, download-and-run-solver: Internal generic functions
Method, download-and-run-solver: Internal generic functions
Method, soft-clauses: Exported generic functions

P
parse-wdimacs-output: Exported functions
print-wcnf: Exported functions

R
rel: Internal functions

S
soft-clauses: Exported generic functions
soft-clauses: Exported generic functions

Jump to:   C   D   F   G   M   P   R   S  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.3 Variables

Jump to:   *  
N   S   T   Y  
Index Entry  Section

*
*base-url*: Internal special variables

N
name: Internal conditions

S
Slot, name: Internal conditions
Slot, soft-clauses: Exported classes
Slot, track: Internal conditions
Slot, year: Internal conditions
soft-clauses: Exported classes
Special Variable, *base-url*: Internal special variables

T
track: Internal conditions

Y
year: Internal conditions

Jump to:   *  
N   S   T   Y  

Previous: , Up: Indexes   [Contents][Index]

A.4 Data types

Jump to:   B   C   D   M   N   P   S   U  
Index Entry  Section

B
build-error: Internal conditions

C
chmod-error: Internal conditions
cl-maxsat: The cl-maxsat system
cl-maxsat: The cl-maxsat package
Class, maxsat-instance: Exported classes
competition-setup-error: Internal conditions
Condition, build-error: Internal conditions
Condition, chmod-error: Internal conditions
Condition, competition-setup-error: Internal conditions
Condition, download-error: Internal conditions
Condition, no-cplex-error: Internal conditions
Condition, unzip-error: Internal conditions

D
download-error: Internal conditions

M
maxsat-instance: Exported classes

N
no-cplex-error: Internal conditions

P
Package, cl-maxsat: The cl-maxsat package

S
System, cl-maxsat: The cl-maxsat system

U
unzip-error: Internal conditions

Jump to:   B   C   D   M   N   P   S   U