##########################################################################
# #
# Combine - an OCaml library for combinatorics #
# #
# Copyright (C) 2012-2014 #
# Remy El Sibaie #
# Jean-Christophe Filliatre #
# #
# This software is free software; you can redistribute it and/or #
# modify it under the terms of the GNU Library General Public #
# License version 2.1, with the special exception on linking #
# described in file LICENSE. #
# #
# This software is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. #
# #
##########################################################################
* Library
The Combine library contains four main modules:
- Dlx: implements Knuth's dancing links
- Zdd: implements Zero-suppressed binary decision diagrams
- Emc: a common interface to modules Dlx and Zdd to solve EMC +
reduction of EMC to SAT
- Tiling: converts a 2D tiling problem into an EMC problem
Usage: the Combine library is packed into a single module Combine, installed
in the subdirectory combine/ of OCaml's standard library. Thus, it must be
used as follows:
ocamlc -I +combine combine.cma <other files>
full documentation : https://www.lri.fr/~filliatr/combine/
* Examples
The distribution contains several example programs:
- queens.ml: solve the N-queens puzzle
- sudoku.ml: well, you haved guessed already
- color.ml: 4-color planar graphs using DLX and SAT (requires OCamlgraph
and an explicit 'make color.opt')
* Tiling language and interpreter
In addition to the library, Combine provides a language to describe 2D tiling
problems and an interpreter (combine) for this language.
Directory tests/ contains various examples of tiling problems (.cmb files).
To execute such a test, just run "combine" on the file.
The grammar of the tiling language is the following:
<file> ::= | decl ... decl
<decl> ::=
| pattern <identifier> = <expr>
| tiles <identifier> = <tile_list>
| problem <identifier> equal <expr> tl = tiles
| assert b = boolean_expr
| print <identifier>
| solve a = algo <identifier> out = output
| count a = algo <identifier>
| dimacs <identifier> <string>
| debug st = state
| timing st = state
| exit
| include <string>
algo ::=
| dlx
| zdd
| sat <string>
state ::=
| on
| off
option ::=
| one
| maybe
| sym
| rot
tiles ::=
| <tile_list>
| <identifier>
tile_list ::=
| [ tile, ..., tile ]
output ::=
| svg_out <string>
| ascii_out
isometry ::=
| id
| rot90
| rot180
| rot270
| vertrefl
| horizrefl
| diag1refl
| diag2refl
tile ::=
| <expr> o = list(option)
expr ::=
| lpar <expr> rpar
| <identifier>
| constant <dim> <bool>
| union <expr> <expr>
| inter <expr> <expr>
| diff <expr> <expr>
| xor <expr> <expr>
| <expr> minus <expr>
| <expr> ampamp <expr>
| <expr> barbar <expr>
| <expr> hat <expr>
| set <expr> <dim> <bool>
| crop <dim> <dim> <expr>
| shift <expr> <dim>
| resize <expr> <dim>
| apply <isometry> <expr>
| <ascii>
bool ::=
| false
| true
boolean_expr::=
| <bool>
| <expr> equal <expr>