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:
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 SatSolver.java interface in the org.tweetyproject.logics.pl.sat package and think about implementing a bridge yourself and contribute it to TweetyProject.
back