miniexact 1.2.7

This is the MiniExact exact cover solver, implementing Donald Knuth's Algorithm X, C, and M using the Dancing Links technique.

miniexact

A minimalistic implementation of Donald Knuth's exact cover solving algorithms. Currently supporting:

• Algorithm X
• Algorithm C
• Algorithm M
• SAT Backend

Features:

• Web and CLI version
• Two input formats: One inspired by Donald Knuth's text representation, one by DIMACS from SAT solving.
• C-code is kept as close to Knuth's description as possible using Macros.
• Extensively hackable
• No dependencies
• SWIG Bindings support (if available on the system), see the Python example.

Usage

Either use the web-version in your browser, the latest universal APE release, or compile yourself. The command line tools expect the algorithm to use (-x, -c, or -m) and the input file(s). If multiple files are given (e.g. using your shell's wildcard), each file is solved separately.

A solution is the list of selected options. You can also print the options as they were listed in the input file with the -p (print) switch.

In order to enumerate all possible solutions, use the -e (enumerate) switch.

You can change the heuristic used internally to a naive one, but the MRV heuristic (the default) is a good choice usually.

Knuth Exact Cover Format

This format is inspired by Donald Knuth's notation in /The Art of Computer Programming Volume 4 Fasicle 5/. You first list all primary (possibly with multiplicity values) and secondary items, then you list all options. This format is well readable and easy to generate and parse.

Example

< a b c d e f g >
c e;
a d g;
b c f;
a d f;
b g;
d e g;

Input Grammar

problem ::= primary_items [ secondary_items ] { option }
primary_items ::= '<' { primary_item } '>'
primary_item ::= ident [ ':' u [ ';' v ] ]
secondary_items ::= '[' { secondary_item } ']'
secondary_item ::= ident
option ::= { ident [ ':' color ] } ';'

DIMACS-inspired Format

This format is optimized to be generated by tools and is a combination of the DIMACS format known from SAT solving and the requirements for Exact Cover problems. You first define the number of primary and secondary items, then you list the options below. No item names are supported, as only integers are used. Colors can be given as negative integers after a secondary item was given.

Example

p xcc 2 1
2 3 -1 0
1 3 -1 0

Input Grammar

problem ::= 'p' ( 'xc' | 'xcc' ) <primary count> <secondary count> options
options ::= { option '0' }
option ::= { primary | secondary }
primary ::= <int>
secondary ::= <int> [ '-'<int> ]

Compiling

Reqirements:

• C Compiler (e.g. GCC or Clang)
• make
• cmake
• Optional: SWIG and Python 2/3

Create a sub-directory, generate a build script and compile the tool. Use something like this:

mkdir build
cd build
cmake ..
make

By default, a Release build is created. To develop the project, using the Debug build is recommended. For this, run cmake using cmake .. -DCMAKE_BUILD_TYPE=Debug.