## Expand description

## 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

Feature | Description |
---|---|

`open_wbo` | Activates MaxSAT solving with Open-WBO |

### Funding

LogicNG for Rust development is funded by the SofDCar project:

## Modules

- Backbone computation.
- Cardinality constraint encoders.
- Various datastructures.
- Tools for analyzing unsatisfiable results.
- Types and datastructures to represent and manage formulas effectively.
- Graphs and Hypergraphs.
- Handlers for more control during some calculations.
- Functions for reading and writing formulas from/to files.
- Offline compilation of formulas for faster online queries.
- Functions, Predicates, and Transformations for formulas.
- Tool for assigning additional information to a formula.
- Pseudo-boolean constraint encoders.
- Solvers for SAT and MaxSAT.
- Additional utility.