A Library for Creating, Manipulating, and Solving Boolean Formulas

THIS IS AN ALPHA VERSION! THE API MAY STILL CHANGE IN SIGNIFICANT WAYS! THE PROGRAM IS NOT FULLY TESTED, DO NOT USE IN PRODUCTION!

Introduction

This is LogicNG for Rust. The original version of LogicNG is a Java Library for creating, manipulating and solving Boolean and Pseudo-Boolean formulas.

Its main focus lies on memory-efficient data-structures for Boolean formulas and efficient algorithms for manipulating and solving them. The library is designed and most notably used in industrial systems which have to manipulate and solve millions of formulas per day. The Java version of LogicNG is heavily used by the German automotive industry to validate and optimize their product documentation, support the configuration process of vehicles, and compute WLTP values for emission and consumption.

Implemented Algorithms

The Rust version of LogicNG currently provides -among others- the following key functionalities:

• Support for Boolean formulas, cardinality constraints, and pseudo-Boolean formulas
• Thread-safe formula factory (in contrast to the Java version)
• Parsing of Boolean formulas from strings or files
• Transformations of formulas, like
  • Normal-Forms NNF, DNF, or CNF with various configurable algorithms
  • Anonymization of formulas
  • Simplification of formulas via subsumption or backbones
• Encoding cardinality constraints and pseudo-Boolean formulas to purely Boolean formulas with a majority of different algorithms
• Solving formulas with an integrated SAT Solver including
  • Fast backbone computation on the solver
  • Incremental/Decremental solver interface
  • Proof generation
  • Optimization with incremental cardinality constraints
• Optimizing formulas with a MaxSAT solver (integrated Open-WBO), activate via feature open_wbo
• Knowledge compilation with BDDs or DNNFs

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.

Whitepaper

If you want a high-level overview of LogicNG and how it is used in many applications in the area of product configuration, you can read our whitepaper.

First Steps

The following code creates the Boolean Formula A and not (B or not C) programmatically.

use logicng::formulas::FormulaFactory;

let f = FormulaFactory::new();
let a = f.variable("A");
let b = f.variable("B");
let not_c = f.literal("C", false);
let formula = f.and(&[a, f.not(f.or(&[b, not_c]))]);

Alternatively you can just parse the formula from a string:

use logicng::formulas::FormulaFactory;

let f = FormulaFactory::new();
let formula = f.parse("A & ~(B | ~C)").expect("Parsing failed");

Or even shorter:

use logicng::formulas::{FormulaFactory, ToFormula};

let f = FormulaFactory::new();
let formula = "A & ~(B | ~C)".to_formula(&f);

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

use logicng::formulas::{FormulaFactory, ToFormula};
use logicng::solver::minisat::MiniSat;

let f = FormulaFactory::new();
let formula = "A & ~(B | ~C)".to_formula(&f);

let nnf = f.nnf_of(formula);
let cnf = f.cnf_of(formula);
let mut miniSat = MiniSat::new();
let result = miniSat.sat();

Features

Funding

LogicNG for Rust development is funded by the SofDCar project: