Introduction

LogicNG is a Java Library for creating, manipulating and solving Boolean and Pseudo-Boolean formulas. It includes 100% Java implementations of popular tools like MiniSAT, CleaneLing, Glucose, PBLib, or OpenWBO.

Its main focus lies on memory-efficient data-structures for Boolean formulas and efficient algorithms for manipulating and solving them. The library is designed to be used in industrial systems which have to manipulate and solve millions of formulas per day.

Philosophy

The most important philosophy of the library is to avoid unnecessary object creation. Therefore formulas can only be generated via formula factories. A formula factory assures that a formula is only created once in memory. If another instance of the same formula is created by the user, the already existing one is returned by the factory. This leads to a small memory footprint and fast execution of algorithms. Formulas can cache the results of algorithms executed on them and since every formula is hold only once in memory it is assured that the same algorithm on the same formula is also executed only once.

Compared to other implementation of logic libraries on the JVM this is a huge memory and performance improvement.

Usage

LogicNG is released in the Maven Central Repository. To include it just add

<dependency>
  <groupId>org.logicng</groupId>
  <artifactId>logicng</artifactId>
  <version>1.6.2</version>
</dependency>

to your Maven POM.

Development Model

The master branch contains the latest release of LogicNG. If you want a stable and well tested version you should choose this branch. The development branch reflects the current state of the next version. This branch will always compile, but code might not be as well tested and APIs may still change before the next release. If you want to try cutting edge features, you can checkout this branch at your own risk. It is not recommended to use the development version for production systems. Larger features will be developed in their own branches and will be merged to the development branch when ready.

Getting Started

Compilation

To compile LogicNG simply run mvn compile to build the parsers and compile the source code. You can build a jar of the library with mvn package or install it in your local maven repository via mvn install.

First Steps

The following code creates the Boolean Formula A and not (B or not C) programatically:

final FormulaFactory f = new FormulaFactory();
final Variable a = f.variable("A");
final Variable b = f.variable("B");
final Literal notC = f.literal("C", false);
final Formula formula = f.and(a, f.not(f.or(b, notC)));

Alternatively you can just parse the formula from a string:

final FormulaFactory f = new FormulaFactory();
final PropositionalParser p = new PropositionalParser(f);
final Formula formula = p.parse("A & ~(B | ~C)");

Once you created the formula you can for example convert it to NNF or CNF or solve it with an instance of MiniSAT:

final Formula nnf = formula.nnf();
final Formula cnf = formula.cnf();
final SATSolver miniSat = MiniSat.miniSat(f);
miniSat.add(formula);
final Tristate result = miniSat.sat();

Frequently Asked Questions

We recently started a Wiki section for a FAQ.

License & Commercial Support

The library is released under the Apache License and therefore is free to use in any private, educational, or commercial projects. Commercial support is available through the German company BooleWorks GmbH - the company behind LogicNG. Please contact Christoph Zengler at [email protected] for further details.

Changelog

Version 1.6.2 (Release January 2020)

• Some improvements to handlers for computations
• New BDD handlers

Version 1.6.1 (Release September 2019)

• A new method for solving a formula with a given literal ordering.
• Minor refactoring of the Formatter super class (no effects on callers).
• Fixed the behaviour of model enumeration with additional variables.

Version 1.6.0 (Release September 2019)

• A new method for generating CNFs directly on the solver instead of using the formula factory. This often leads to a faster generation and reduced Heap consumption but with the loss of caching
• The standard MiniSat-based solvers can now directly efficiently compute a backone. No extra solver is required anymore
• The current formula on a MiniSat-based solver can be extracted
• BDD factory can now be extended externally

Version 1.5.2 (Release July 2019)

• Fixed caching behaviour when using a sat() call without assumptions after a call with assumptions
• Clarified behaviour of the Backbone object

Version 1.5.1 (Release May 2019)

• Introduced a new FormulaHelper class for small utility methods on formulas
• Added a new NNF predicate
• Fixed an unspecified behaviour in SATPredicate
• Fixed a small performance issue in the new backbone solver
• Fixed a bug in a special case of the CNF transformation of a pseudo-Boolean constraint

Version 1.5.0 (Release March 2019)

• Algorithm & data structures for efficiently computing backbones of formulas
• Data structures for UBTrees in order to efficiently identify sub- and supersets
• CNF and DNF subsumption as formula transformations
• Backbone simplifier (compute and propagate the backbone of a formula)
• A new sorted formula formatter which respects a given variable ordering when printing formulas
• Minor code refactorings and improvements
• Deprecation of CleaneLing - this solver will be removed in future versions.

Version 1.4.1 (Release December 2018)

• Some refactorings for unit tests on Windows regarding encodings
• The Quine-McCluskey implementation does not yield CNF auxiliary variables anymore
• Fixed a minor bug in the generation of incremental cardinality constraints

Version 1.4.0 (Release June 2018)

• BDD package (based on Buddy) for creating, manipulating, and writing BDDs
  • Creation of BDDs from LogicNG formulas
  • CNF, DNF transformation of BDDs
  • Restriction, existential & universal quantifier elimination
  • Model counting & enumeration
  • Different static variable ordering heuristics (FORCE, DFS, BFS, MinMax)
  • Writing BDDs in the GraphViz .dot format
• Quine-McCluskey Implementation for minimizing canonical DNFs
• New formula transformation for anonymizing formulas
• Internal parser and IO improvements. Variables can now start with a digit.

Version 1.3.1 (Release January 2018)

• Huge performance boost in the model enumeration of MiniSat
• New formula transformation which imports formulas in another formula factory
• Small bugfix for a trivial case in DRUP

Version 1.3 (Release October 2017)

• MiniSat and Glucose have a new option for proof tracing. A DRUP implementation stores all the necessary information for generating a proof for unsatisfiable formulas after solving them. The new method can be found in the SAT solver class: unsatCore()
• Unsat Cores are now parametrized with the proposition type
• A new simplifier which applies the distributive law was added: DistributiveSimplifier
• Some minor bug-fixes in handling corner cases of cardinality and pseudo-Boolean constraints

Version 1.2 (Release July 2017)

• Introduced an extended formula factory which is able to return to a previously saved state and delete old formulas (and get them garbage collected)
• A simple data structure for generic graphs including algorithms for connected components and maximal cliques
• Improved IO (Writers for formulas, Dimacs CNFs, and graphs)
• SAT solvers can now track the currently known variables
• Updated to ANTLR 4.7
• Various smaller bugfixes

Version 1.1 (Release August 2016)

• Implemented cardinality constraint encodings and pseudo-Boolean constraints encodings of PBLib
• Incremental cardinality constraints, including the possibility to add cardinaliy constraints to the solver without introducing new formula factory variables
• Different MUS algorithms