Skip to content
DPLL boolean satisfiability solver for .NET
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
doc
src
.editorconfig
.gitattributes
.gitignore
.travis.yml
COPYING.txt
GitVersion.yml
README.md
appveyor.yml
build.ps1
build.sh

README.md

NanoByte SAT Solver

NuGet API documentation Build status
NanoByte SAT Solver is a DPLL Boolean Satisfiability Solver for .NET.

Usage

Add a reference to the NanoByte.SatSolver NuGet package to your project. It is available for .NET Framework 2.0+ and .NET Standard 1.0+.

You need to choose the underlying type to use for Literals in Boolean Formulas. This will often be int or string but you can also use any other type that implements the IEquatable<T> interface. You can then create an instance of Solver<T>:

var solver = new Solver<string>();

The library enables you to express Boolean Formulas using implicit casting and operators for human-friendly sample and test code:

Literal<string> a = "a", b = "b", c = "c", d = "d";
var formula = (a | b) & (!a | c) & (!c | d) & a;

For constructing Formulas at run-time you can use a collection-like interface instead:

var formula = new Formula<string>
{
    new Clause<string> {Literal.Of("a"), Literal.Of("b")},
    new Clause<string> {Literal.Of("a").Negate(), Literal.Of("c")},
    new Clause<string> {Literal.Of("c").Negate(), Literal.Of("d")},
    new Clause<string> {Literal.Of("a")}
};

Finally, you can use the solver to determine whether a Formula is satisfiable:

bool result = solver.IsSatisfiable(formula);

When the Solver needs to choose a Literal to assign a truth value to during backtracking, it simply picks the first unset Literal from the list. You can replace this with your own domain-specific logic for better performance by deriving from Solver<T> and overriding the ChooseLiteral() method.

Building

The source code is in src/, a project for API documentation is in doc/ and generated build artifacts are placed in artifacts/.

You need Visual Studio 2017 to perform a full build of this project.
You can build for .NET Standard on Linux using just the .NET Core SDK 2.1+. Additionally installing Mono 5.10+ allows you to also build for .NET Framework. The build scripts will automatically adjust accordingly.

Run .\build.ps1 on Windows or ./build.sh on Linux. These scripts take a version number as an input argument. The source code itself contains only contains dummy version numbers. The actual version is picked by continuous integration using GitVersion.

Contributing

We welcome contributions to this project such as bug reports, recommendations and pull requests.

This repository contains an EditorConfig file. Please make sure to use an editor that supports it to ensure consistent code style, file encoding, etc.. For full tooling support for all style and naming conventions consider using JetBrain's ReSharper or Rider products.

You can’t perform that action at this time.