arminbiere/lingeling

Lingeling SAT Solver

C

111

9 commits

updated Mar 12, 2024

See the code

README

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

Not written in Markdown, so it's shown here as plain text — view it formatted on GitHub.

Significant stargazers

Oleg Höfling

32 followers · starred May 2019

Andrew Teylu

28 followers · starred May 2018

archaistvolts

70 followers · starred Sep 2025

danflapjax

4 followers · starred Sep 2020

arminbiere/lingeling

Lingeling SAT Solver

C

111

9 commits

updated Mar 12, 2024

See the code

README

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

Not written in Markdown, so it's shown here as plain text — view it formatted on GitHub.

Significant stargazers

Oleg Höfling

32 followers · starred May 2019

Andrew Teylu

28 followers · starred May 2018

archaistvolts

70 followers · starred Sep 2025

danflapjax

4 followers · starred Sep 2020

Languages

C

98.8%

Shell

1.2%