Sat4j is a full featured boolean reasoning library designed to bring state-of-the-art SAT technologies to the Java Virtual Machine.
Sat4j is a java library for solving boolean satisfaction and optimization problems. It can solve SAT, MAXSAT, Pseudo-Boolean, Minimally Unsatisfiable Subset (MUS) problems. Being in Java, the promise is not to be the fastest one to solve those problems (a SAT solver in Java is about 3.25 times slower than its counterpart in C++), but to be full featured, robust, user friendly, and to follow Java design guidelines and code conventions (checked using static analysis of the source code). The library is designed for flexibility, by using heavily the decorator and strategy design patterns. Furthermore, Sat4j is open source, under the dual business friendly Eclipse Public License and academic friendly GNU LGPL license.
To get an idea of what can be done using Sat4j, you might want to take a look at Sat4j case studies (draft).
Over the years, Sat4j has been used by numerous research groups, especially in software engineering, and has been included in the curriculum of many constraint programming, AI or software verification classes (see all papers citing Sat4j's system description/see all papers mentioning Sat4j/see all web pages mentioning Sat4j).
