Sat4j
the boolean satisfaction and optimization library in Java
 
Overview
Top
ProductDescriptionTarget AudienceProductionInput Format
Core Lightweight constraint programming with a SAT solver. Java developers, Researchers Dimacs CNF or AIG
SAT SAT Toolkit in Java. SAT researchers Dimacs CNF or AIG
Pseudo Pseudo-boolean Solvers. Java developers, Researchers PB evaluation format
Maxsat MAX SAT Solvers based on reduction to Pseudo-boolean optimization problems. Java developers, Researchers Max SAT evaluation format
CSP CSP solvers based on a translation into SAT. Researchers Ongoing development CSP competition XML format
Sudoku Demo SAT-based Sudoku generator and solver. Sudoku lovers Most common Sudoku online formats
Caution Maven users The group and artifact ids of sat4j has changed in released 2.3.3 to allow sat4j artifacts to be distributed by OW2. They start now with org.ow2.sat4j instead of org.sat4j. Older releases will stay available under the previous group and artifact ids.
SAT4J Core
Top
  • Lightweight constraint programming with a SAT solver. Ships with Eclipse/Equinox 3.4+ as OSGi bundle org.sat4j.core.
  • Maven declaration: 
    <dependency>
  <groupId>org.ow2.sat4j</groupId>
  <artifactId>org.ow2.sat4j.core</artifactId>
  <version>2.3.4</version>
</dependency>
  • Input format: Dimacs CNF or AIG
  • API: Visit the JavaDoc
SAT4J SAT
Top
  • SAT Toolkit in Java. Offers a command line interface to SAT4J core allowing to easily test various SAT solver configurations.
  • Maven declaration: 
    <dependency>
  <groupId>org.ow2.sat4j</groupId>
  <artifactId>org.ow2.sat4j.sat</artifactId>
  <version>2.3.4</version>
</dependency>
  • Input format: Dimacs CNF or AIG
  • API: Visit the JavaDoc
  • Dependencies: SAT4J Core, Apache Jakarta Commons (BeanUtils, CLI)
SAT4J Pseudo
Top
  • Pseudo-boolean Solvers. Ships with Eclipse/Equinox 3.4+ as OSGi bundle org.sat4j.pb.
  • Maven declaration: 
    <dependency>
  <groupId>org.ow2.sat4j</groupId>
  <artifactId>org.ow2.sat4j.pb</artifactId>
  <version>2.3.4</version>
</dependency>
  • Input format: PB evaluation format
  • API: Visit the JavaDoc
  • Dependencies: SAT4J Core
SAT4J Maxsat
Top
  • MAX SAT Solvers based on reduction to Pseudo-boolean optimization problems.
  • Maven declaration: 
    <dependency>
  <groupId>org.ow2.sat4j</groupId>
  <artifactId>org.ow2.sat4j.maxsat</artifactId>
  <version>2.3.4</version>
</dependency>
  • Input format: Max SAT evaluation format
  • API: Visit the JavaDoc
  • Dependencies: SAT4J Core, SAT4J PB, Apache Jakarta Commons
SAT4J CSP
Top
  • CSP solvers based on a translation into SAT.
  • Maven declaration: 
    <dependency>
  <groupId>org.ow2.sat4j</groupId>
  <artifactId>org.ow2.sat4j.csp</artifactId>
  <version>2.3.4</version>
</dependency>
  • Input format: CSP competition XML format
  • API: Visit the JavaDoc
  • Dependencies: SAT4J Core, Rhino
Sudoku Demo
Top
  • SAT-based Sudoku generator and solver. Contributed by Ivor Spence. Also available online as an applet
  • Input format: Most common Sudoku online formats
  • Dependencies: SAT4J Core. Ships as a all-in-one package (SAT4J core included).