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, Glucose, PBLib, or OpenWBO. For details about this core library refer to LogicNG.

This library provides two parsers for propositional formulas (LogicNGPropositionalParser) and pseudo-boolean formulas (LogicNGPseudoBooleanParser) which are based on the ANTLR parser generator.

Usage

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

<dependency>
  <groupId>org.logicng</groupId>
  <artifactId>logicng-parser-j8</artifactId>
  <version>2.6.0</version>
</dependency>

to your Maven POM. If you are using Java 11, use logicng-parser-j11 instead as artifactId.

For parsing a formula, you just create one of the two parsers and call parse on it:

import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
import org.logicng.io.parsers.PropositionalParser;
import org.logicng.io.parsers.PseudoBooleanParser;

FormulaFactory f = new FormulaFactory();
PropositionalParser propositionalParser = new PropositionalParser(f);
Formula formula1 = propositionalParser.parse("A & ~(B | ~C)");

PseudoBooleanParser pseudoBooleanParser = new PseudoBooleanParser(f);
Formula formula2 = pseudoBooleanParser.parse("2 * A + 3 * B - 2 * C <= 3");

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.