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


Brought to you by




Supported by

back

Integration of SAT solvers

Tweety 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.

Tweety 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:

import net.sf.tweety.logics.pl.sat.*;
...
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. Tweety also supports the integration of command-line based solvers such as Lingeling. If you have Lingeling installed in your system you can set it as your default SAT solver via:

SatSolver.setDefaultSolver(new LingelingSolver(pathToLingeling));

If your favorite SAT solver is not supported, please have a look at the SatSolver.java interface in the net.sf.tweety.logics.pl.sat package and think about implementing a bridge yourself and contribute it to Tweety.




back



Last updated 11.01.2016, Matthias Thimm