These are the sources of the SAT solver Lingeling. The file VERSION contains the current version number. To build everything issue ./configure.sh && make This will build the library 'liblgl.o', the sequential solver 'lingeling', its parallel version 'plingeling', and the cube & conquer solvers 'treengeling' and 'ilingeling'. If you have a compiled copy of the AIGER library in '../aiger/', which can be obtained from 'http://fmv.jku.at/aiger' then the bounded model checker 'blimc' will also be build. If you need proof support add and compile the 'druplig' library in '../druplig/' from 'http://fmv.jku.at/druplig'. If you want to add local search (particularly useful for 'treengeling') add and compile 'yalsat' in '../yalsat/' from 'http://fmv.jku.at/yalsat'. Copyright, authors and license are described in COPYING. With release 'bcj', which in essence is the version submitted to the SAT Competition 2018, we moved to an MIT style license. A more recent version of Lingeling might be found at http://fmv.jku.at/lingeling and this site might also contain more documentation. Thu May 17 11:45:27 CEST 2018