-- Tarmo release 121023 --

Copyright (c) 2008-2011  Matti Niemenmaa, Siert Wieringa
Copyright (c) 2012       Siert Wieringa
                         Aalto University, Finland

Tarmo includes a modified version of MiniSAT, which is licensed under 
an MIT style license. This license also applies also to all other parts 
of the Tarmo distribution.

The completely new version of Tarmo is tightly integrated with the latest 
MiniSAT version from Niklas Sörensson's repositories. This new version of Tarmo
is easy to integrate in any kind of application of incremental SAT solvers,
particularly those that are already using MiniSAT.

Tarmo release 121023 contains the basic Tarmo solver and a Tarmo based MUS 
finder. The basic solver can be used from the command line to solve iCNF files.

Similarly to the MiniSAT CMake super-project Tarmo uses cmake. Take the 
following steps to setup Tarmo:

    Download Tarmo release 121023
    Unpack the files
    Create a directory to build Tarmo in
    In the build directory execute cmake < path to source >
    Once cmake completes execute make

To include Tarmo in your application create an instance of the TarmoSolver
class. Applications that are already build around MiniSAT can use the 
CompatibleSolver class as a drop-in replacement for MiniSAT.
-- Tarmo at Hardware Model Checking Competition 2012 (HWMCC12) --

To illustrate that Tarmo can be easily integrated into many applications of 
incremental SAT solvers it was used to parallelize the Bounded Model Checking 
(BMC) algorithm inside Niklas Sörensson's TIP model checker. The result was 
submitted to Hardware Model Checking Competition 2012 (HWMCC12). The most
notable results Tarmo achieved were:

    Tarmo ranked second on satisfiable safety instances
    Tarmo ranked first on satisfiable liveness instances