1.2.0

Drastically improves performance for small instances by using purely internal memory data structures.

Performance

Below is the running time for the N-Queens for v1.0, v1.1, and v1.2. As is evident, it is an improvement all across the board. Furthermore, the change in v1.1 that improved running time for large instances but severely crippled the small ones has been mitigated.

N	7	8	9	10	11	12	13	14	15	16
v1.0 (s)	7.4s	8.2s	7.8s	9.4s	28.5s	28.5s	119s	660s	3944s	31017s
v1.1 (s)	19.3s	25.6s	32.2s	39.5s	48.7s	58.4s	751s	1296s	4270s	24544s
v1.2 (s)	0.1s	0.2s	0.4s	0.8s	3.1s	14.8s	82.7s	502s	3337s	23127s

Domain

The global domain over which one works can now be set as a label_file in a global variable.

• adiar_set_domain(label_file dom)
  Set the global domain variable.
• adiar_has_domain()
  Whether a global domain already is set.
• adiar_get_domain()
  Obtain the current label_file that acts as the global domain (assuming adiar_has_domain() evaluates to true).

Binary Decision Diagrams

New Features

• bdd_builder
  A new class to replace using the node_writer directly. This allows you to much more naturally construct BDDs bottom-up by hiding away several details. Furthermore, it makes use of exceptions rather than immediately terminating assertions.
• bdd_from(zdd A)
  Converts from a ZDD to a BDD using the global domain.
• bdd_equal(bdd f, bdd g)
  Alternative to using the == operator.
• bdd_unequal(bdd f, bdd g)
  Alternative to using the != operator.
• bdd_varprofile(bdd f)
  Obtain a label_file containing all of the variables present in a BDD.

Bug Fixes

• bdd_nithvar(label_t i) and bdd_ithvar(label_t i)
  Is now marked as canonical and so can be used with the linear-scan equality checking.
• Fixed the reduction phase may use 2 MiB more memory than is available.

Zero-suppressed Decision Diagrams

New Features

• zdd_builder
  A new class to replace using the node_writer directly. This allows you to much more naturally construct ZDDs bottom-up by hiding away several details. Furthermore, it makes use of exceptions rather than immediately terminating assertions.
• zdd_complement(zdd A)
  Complementation within the global domain.
• zdd_from(bdd f)
  Converts from a BDD to a ZDD using the global domain.
• zdd_varprofile(zdd A)
  Obtain a label_file containing all of the variables present in a ZDD.

Bug Fixes

• zdd_ithvar(label_t i)
  Is now marked as canonical and so can be used with the linear-scan equality checking.
• Fixed the reduction phase may use 2 MiB more memory than is available.
• DOT files are now properly produced with the terminals printed as Ø and {Ø}.

Statistics

New Features

• Statistics have been heavily extended with information on how often each type of auxiliary data structures (internal or external) have been used.
• All statistics variables are now fixed-precision numbers (using the CNL library) making sure there are no overflows in the provided numbers.
• adiar_statsreset()
  Reset all statistics values back to 0.

Bug Fixes

• Fixed fine grained statistics (ADIAR_STATS_EXTRA) are turned on when only coarse-grained statistics (ADIAR_STATS) was desired.

Deprecations

The word sink has been replaced with the word terminal that is more commonly used in the context of decision diagrams.

• adiar/data.h
  • create_sink_uid(bool val) -> create_terminal_uid(bool val)
  • create_sink_ptr(bool val) -> create_terminal_ptr(bool val)
  • create_sink(bool val) -> create_terminal(bool val)
• adiar/bdd.h
  • is_sink(bdd f) -> is_terminal(bdd f)
  • bdd_sink(bool val) -> bdd_terminal(bool val)
• adiar/zdd.h
  • is_sink(zdd A) -> is_terminal(zdd A)
  • zdd_sink(bool val) -> zdd_terminal(bool val)

Breaking Changes

The terminal predicates is_any, is_true and is_false with the prior is_sink(zdd A, pred) functions were too complicated. The above performance improvements allows us for a much simpler (and faster) implementation. Deprecation was not possible due to name conflicts with their replacements below. Considering the niche usage of this, it does not seem to warrant an increment in version number.

• adiar/data.h
  • is_sink(ptr_t p), is_true(ptr_t p), and is_false(ptr_t p).
• adiar/bdd.h
  • is_sink(bdd f), is_true(bdd f) and is_false(bdd f).
• adiar/zdd.h
  • is_sink(zdd A), is_null(zdd A) and is_empty(zdd A).

Contributors

• Steffan Sølvsten ( @SSoelvsten )
• Anna Blume Jakobsen ( @AnnaBlume99 )
• Jaco van de Pol ( @jacopol )

Also thanks to Erik Funder Carstensen ( @halvko ) for fixing a few compiler warning in statistics.

License

Adiar uses the TPIE library which is licensed under LGPL v3, and so by extension any binary file with Adiar is covered by the very same license.