##########################################################################

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

  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:

::= | decl ... decl

::= | pattern = | tiles = <tile_list> | problem equal tl = tiles | assert b = boolean_expr | print | solve a = algo out = output | count a = algo | dimacs | debug st = state | timing st = state | exit | include

algo ::= | dlx | zdd | sat

state ::= | on | off

option ::= | one | maybe | sym | rot

tiles ::= | <tile_list> |

tile_list ::= | [ tile, ..., tile ]

output ::= | svg_out | ascii_out

isometry ::= | id | rot90 | rot180 | rot270 | vertrefl | horizrefl | diag1refl | diag2refl

tile ::= | o = list(option)

expr ::= | lpar rpar | | constant | union | inter | diff | xor | minus | ampamp | barbar | hat | set | crop | shift | resize | apply |

bool ::= | false | true

boolean_expr::= | | equal