The Next Generation Logic Library

Related tags

Science LogicNG
Overview

wercker status Coverage Status License Version

logo

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.

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>2.0.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.

Comments
  • Memory requirements

    Memory requirements

    I am trying to convert my logic representation of SHA1 hash algorithm into LogicNG and run CNF. But I am getting Java heap space error, even when allocating 24GB to heap space.

    Is there a way to debug memory usage? I basically have a boolean graph with (and, xor and not) with 100 thousand nodes, building LogicNG formula works without any problems, but CNF algorithm fails on memory usage.

    My goal is to feed the results to SAT solver.

    opened by exander77 10
  • Out of memory issue

    Out of memory issue

    The program will throw an Out Of Memory error if the formula has many variables(e.g. more than 200 variables). java.lang.OutOfMemoryError: Java heap space at java.util.LinkedHashMap.createEntry(Unknown Source) at java.util.HashMap.addEntry(Unknown Source) at java.util.LinkedHashMap.addEntry(Unknown Source) at java.util.HashMap.put(Unknown Source) at java.util.HashSet.add(Unknown Source) at org.logicng.formulas.FormulaFactory.addFormulaOr(FormulaFactory.java:900) at org.logicng.formulas.FormulaFactory.condenseOperandsOr(FormulaFactory.java:812) at org.logicng.formulas.FormulaFactory.constructOr(FormulaFactory.java:520) at org.logicng.formulas.FormulaFactory.or(FormulaFactory.java:477) at org.logicng.transformations.cnf.CNFFactorization.distribute(CNFFactorization.java:109) at org.logicng.transformations.cnf.CNFFactorization.distribute(CNFFactorization.java:106) at org.logicng.transformations.cnf.CNFFactorization.distribute(CNFFactorization.java:106) at org.logicng.transformations.cnf.CNFFactorization.apply(CNFFactorization.java:66) at org.logicng.transformations.cnf.CNFFactorization.apply(CNFFactorization.java:52) at org.logicng.formulas.Formula.transform(Formula.java:191) at org.logicng.formulas.Formula.cnf(Formula.java:182) at org.logicng.solvers.MiniGSat.add(MiniGat.java:154) at org.logicng.solvers.sat.Test.parseRules(Test.java:94) at org.logicng.solvers.sat.Test.testAssume(Test.java:66) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source) at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source) at java.lang.reflect.Method.invoke(Unknown Source) at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:50) at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12) at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:47) at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17) at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:325) at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:78) at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:57) at org.junit.runners.ParentRunner$3.run(ParentRunner.java:290) at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:71)

    opened by xiaomeyu 9
  • [Feature request] implement QuineMcClusky algortihm

    [Feature request] implement QuineMcClusky algortihm

    opened by axkr 7
  • Add JavaDoc to

    Add JavaDoc to "phase"

    I am reading https://github.com/logic-ng/LogicNG#first-steps:

    final Literal notC = f.literal("C", false);

    The documentation states that phase is a Boolean parameter. There is no documentation on the phase in README.md and not at the JavaDoc of literal.

    I wonder why

    a) phase is not en enum? An enum makes the possibilities clear. Currently with false I don't know whether there is no phase processing, if its a phase, where all variables are false, an initialization phase, ... - Reading the code I would have set it to true, but I am not sure.

    b) There is no literal creator without any phase parameter (and then setting a default phase)

    Would is be, additionally, possible to describe the phase in the README.md file?

    (Issue created in my the context of my free-time project JabRef)

    opened by koppor 6
  • [Question] How to reduce syntactic size of a formula

    [Question] How to reduce syntactic size of a formula

    Hi,

    Thanks for making your package available, it's a nice piece of software. I'm trying to minimize some boolean formulas, with the metric that resulting syntactic tree should have as few nodes as possible. Part of the goal on my test set is the fact some atoms in formulas disappear, as they are asserted in both forms (a OR !a => true, a AND !a =>false). This is not immediately obvious, the formulas are pretty large, so I'm trying to use your package for this.

    I've tried running MCQ, but the conversion to what looks like CNF makes some of my formulas blow up in size; this is not ideal. I'm thinking of trying MCQ (which should always be better than CNF, right ?) then DNF and choosing the smallest, iff. it is syntactically smaller than my original formula.

    And wrapping the whole thing so if some step/transformation blows up, just skip it and choose from remaining candidates.

    But maybe there are better ways to do this ?

    Thank you

    opened by yanntm 6
  • [Question] enumerateAllModels() method - Is there an Option for order of output?

    [Question] enumerateAllModels() method - Is there an Option for order of output?

    In the enumerateAllModels() methods, is there an option for the preferred "solution output order"? I.e. if I would like to get the results with the most "True" values for the variables first or the results with the most "False" values for the variables? Something like an "ascending" or "descending" sort order?

    opened by axkr 6
  • cnf() reorders the variables

    cnf() reorders the variables

    In this JUnit test case the cnf() method reorders the variables and the JUnit test fails:

    	public void testLogicNGCNF() {
		final FormulaFactory f = new FormulaFactory();
		final Variable x = f.variable("x");
		final Variable y = f.variable("y");
		final Literal notX = f.literal("x", false);
		final Literal notY = f.literal("y", false);
		// x & ~y | ~x & y
		final Formula formula = f.or(f.and(x, notY), f.and(notX, y)).cnf();
		assertEquals("(x | y) & (~x | ~y)", formula.toString());
	}

    See: Symja JUnit tests

    opened by axkr 6
  • Improve discoverability of features

    Improve discoverability of features

    Currently the only documentation apart from JavaDoc is the "Getting Started" section in the README. As JavaDoc is great when you know something exists but terrible if you don't it would be great to have a way to learn about features. So for example I just learned about the Anonymizer and the BackboneSimplifier by looking through closed issues. This is not the best experience. Even a list with features and classnames would be good.

    opened by rohte 5
  • Changing variable value after parsing formula

    Changing variable value after parsing formula

    Hello, I was wondering if there's a way to change a variable's value after parsing a formula, for example: After parsing ("A & ~(B | ~C)"), is there a way to give "A" the value "true", and then solve it?

    In other words, to only get the assignments where A is true, without using enumerateAllModels().

    opened by m-ajmone 5
  • Performance of QMC

    Performance of QMC

    Hi, should calling QMC on this really crash it ? I understand there are many variables, but still.

    (a0 | a1) & (a2 | a3) & (a4 | a5) | (a6 | a7) & (a8 | a9) | a10 | a11 | a12

    Would there be a way to detect and throw/exit when the algorithm is going haywire ? e.g. a timeout or max rewritten size or such added to the QMC API. That would be nicer than wrapping invocations with a thread + external timeout, which is what I'm currently considering.

    opened by yanntm 5
  • Formula immutable?

    Formula immutable?

    Schönen guten Tag zusammen,

    ich hatte es Steffen neulich mal per Skype angekündigt und jetzt hier das passende Issue. Im Commit 1e7e0013206573750d12e9c5e9590e36a51fd51f haben wir eine Klasse eingecheckt die aus unserer Sicht einen Bug produziert.

    Wir haben versucht das ganze möglicht minimal zu machen, soll heißen, der Code tut eigentlich nichts sinnvolles mehr und wir haben möglichst viel weggelassen. Was jetzt übrig ist sollte schon fast minimal sein.

    Was passiert im Grunde?: Wir basteln Formeln hin und her zusammen und bauen neue, Formula ist ja meines Wissens nach zunächst mal immutable. Dann wollen wir aus einer Formel eine neue berechnen indem wir Teile aus der bisherigen Formel rausstreichen. Dabei gelingt es uns (sollte es das?) die ursprüngliche Formel zu verändern indem wir ihre f.literals() verändern. Das allein ist ja schon unschön.

    Dann verlassen wir die ganze Methode und machen einen Äquivalenzcheck auf zwei anderen Formeln. LogicNG sagt dann am Ende das Z = Z & ~X eine Tautologie sei.

    Guckt euch das Beispiel mal an, wir haben echt lange nach dem Problem gesucht und haben für unseren Fall jetzt auch einen Fix, aber so wahnsinnig intuitiv ist das alles für uns nicht was da abläuft.

    Wenn man auf Java8 umstellt lässt sich der Bug auch mit Streams und Lambdas erzeugen, könnte man auch gleich mal angucken was da passiert.

    Liebe Grüße, Daniel und Ivo

    opened by palaziv 5
Releases(v2.4.1)
Owner
LogicNG
The Next Generation Logic Library
LogicNG
GitHub
JGraphX - Library for visualizing (mainly Swing) and interacting with node-edge graphs.

JGraphX This project is end of life. We don't properly support Maven or publish to Maven Central. If that's an issue, use https://github.com/vlsi/jgra

JGraph 634 Jan 5, 2023
The foundational library of the Morpheus data science framework

Introduction The Morpheus library is designed to facilitate the development of high performance analytical software involving large datasets for both

Zavtech Systems 226 Dec 20, 2022
A 3D chart library for Java applications (JavaFX, Swing or server-side).

Orson Charts (C)opyright 2013-2020, by Object Refinery Limited. All rights reserved. Version 2.0, 15 March 2020. Overview Orson Charts is a 3D chart l

David Gilbert 96 Sep 27, 2022
Java dataframe and visualization library

Tablesaw Overview Tablesaw is Java for data science. It includes a dataframe and a visualization library, as well as utilities for loading, transformi

Tablesaw 3.1k Jan 7, 2023
XChart is a light-weight Java library for plotting data.

XChart XChart is a light weight Java library for plotting data. Description XChart is a light-weight and convenient library for plotting data designed

Knowm 1.3k Dec 26, 2022
Nzyme is a free and open next-generation WiFi defense system.

Nzyme is a free and open next-generation WiFi defense system.

Lennart Koopmann 1.1k Jan 1, 2023
OpenAPI Generator allows generation of API client libraries (SDK generation), server stubs, documentation and configuration automatically given an OpenAPI Spec (v2, v3)

OpenAPI Generator Master (5.4.x): 6.0.x (6.0.x): ⭐ ⭐ ⭐ If you would like to contribute, please refer to guidelines and a list of open tasks. ⭐ ⭐ ⭐ ‼️

OpenAPI Tools 14.8k Dec 30, 2022
Minecraft configurable plugin , which sends messages the first time a player logs into the server or the next time they log in.

JoinMessages Minecraft configurable plugin , which sends messages the first time a player logs into the server or the next time they log in or leave.

ᴠᴀʟᴇɴᴛɪɴ ᴢʜᴇʟᴇᴠ 6 Aug 30, 2022
React Native FBSDK Next

React Native FBSDK Next This project aims to keep continuity of the React Native FBSDK from Facebook. As Facebook dropped support from it. As a commun

Marcos Bérgamo 485 Jan 6, 2023
TransitScheduler - a command line tool that can read .json data formulated for tracking transit patterns to a multithreaded concurrent simulation of passengers boarding and unboarding trains that constantly move to the next station on the line. The trick here, is that two trains cannot occupy the same station at any time.

TransitScheduler - a command line tool that can read .json data formulated for tracking transit patterns to a multithreaded concurrent simulation of passengers boarding and unboarding trains that constantly move to the next station on the line. The trick here, is that two trains cannot occupy the same station at any time.

Emmet Hayes 1 Dec 2, 2022
tuya-spring-boot-starter helps you efficiently create cloud development projects regarding the OpenAPI or message subscription capabilities. You can put all the focus on business logic without taking care of server-side programming nor relational databases.

English | 中文版 tuya-spring-boot-starter helps you efficiently create cloud development projects regarding the OpenAPI or message subscription capabilit

Tuya 37 Dec 26, 2022
Mindustry java mod that adds a redstone-like wire-based logic system, tailored for making circuits.

See Esoterum-Solutions for builds 0.0-1.2 A small Mindustry Java mod that adds a wire-based logic system tailored for building circuits. New content s

null 36 Oct 25, 2022
Logic-less and semantic Mustache templates with Java

Handlebars.java Logic-less and semantic Mustache templates with Java Handlebars handlebars = new Handlebars(); Template template = handlebars.compile

Edgar Espina 1.3k Dec 23, 2022
Cadence is a distributed, scalable, durable, and highly available orchestration engine to execute asynchronous long-running business logic in a scalable and resilient way.

Cadence This repo contains the source code of the Cadence server and other tooling including CLI, schema tools, bench and canary. You can implement yo

Uber Open Source 6.5k Jan 4, 2023
Logisim-evolution is educational software for designing and simulating digital logic circuits

Branch master: Branch develop: Logisim-evolution Table of contents Features Requirements Downloads Nightly builds (unstable) Pictures of Logisim-evolu

null 3k Jan 4, 2023
Problems of Data Structure from basics are covered here for interview preparation and logic building. Basic programming problems and so many interview based leetcode problems are present. Every program is written to solve problem in as optimized way as possible.

Data Structure in Java Problem Solving ??‍?? Problems of Data Structure from basics are covered here for interview preparation and logic building. Bas

Sahil Batra 7 May 23, 2022
Simulates FGO combat logic (only ally)

FGO模拟器 制作自定义单位时，请主要依照FGO的逻辑来写。 虽然可以写出FGO没有的从者、礼装，但是除非符合逻辑否则程序会做什么我也不知道。 另外这个小程序没有任何联网功能，我也不准备录入所有东西的数据，所以请自己制作需要的部件~ 未来大概就只在github随缘更新，但是现有的制作器基本支持写出绝

Yome 24 Dec 19, 2022
cglib - Byte Code Generation Library is high level API to generate and transform Java byte code. It is used by AOP, testing, data access frameworks to generate dynamic proxy objects and intercept field access.

cglib Byte Code Generation Library is high level API to generate and transform JAVA byte code. It is used by AOP, testing, data access frameworks to g

Code Generation Library 4.5k Jan 8, 2023
sql2o is a small library, which makes it easy to convert the result of your sql-statements into objects. No resultset hacking required. Kind of like an orm, but without the sql-generation capabilities. Supports named parameters.

sql2o Sql2o is a small java library, with the purpose of making database interaction easy. When fetching data from the database, the ResultSet will au

Lars Aaberg 1.1k Dec 28, 2022
Thumbnailator - a thumbnail generation library for Java

March 11, 2021: Thumbnailator 0.4.14 has been released! See Changes for details. Thumbnailator is now available through Maven! What is Thumbnailator?

Chris Kroells 4.5k Jan 5, 2023