A comprehensive collection of Java libraries for logical aspects of artificial intelligence and knowledge representation
Home Libraries Downloads Documentation Newsletter Web Interfaces Contact

Brought to you by

Supported by


Integration of SAT solvers

TweetyProject supports the integration of different SAT solvers in order to perform reasoning tasks in e.g. propositional logic. It is required that at least one SAT solver is explicitly configured as default solver.

TweetyProject has built-in support for the Java-based SAT solver Sat4j which is also set as the default SAT solver. However, whenever you perform a reasoning task that involves a SAT solver, a warning message is printed out that no SAT solver is configured and Sat4j is used as a default. If you do not care about performance issues and only want to get rid of the warning message, you should configure Sat4j as your default SAT solver explicitly. To do that, simply add the following lines somewhere before you invoke your reasoning task for the first time:

SatSolver.setDefaultSolver(new Sat4jSolver());

However, depending on your reasoning tasks it is recommend that you either configure Sat4jSolver further or set another SAT solver as your default solver. TweetyProject also supports the integration of command-line based solvers such as Lingeling. If you have Lingeling or another SAT solver installed in your system you can set it as your default SAT solver via:

SatSolver.setDefaultSolver(new CmdLineSatSolver(pathToSolver));

CmdLineSatSolver supports most command-line based SAT solvers that use the Dimacs input format. If your favorite SAT solver is not supported, please have a look at the interface in the package and think about implementing a bridge yourself and contribute it to TweetyProject.


Last updated 28.01.2021, Anna Gessler | Terms