SimpleSAT 1.0.1

.NET 6.0
dotnet add package SimpleSAT --version 1.0.1
NuGet\Install-Package SimpleSAT -Version 1.0.1
This command is intended to be used within the Package Manager Console in Visual Studio, as it uses the NuGet module's version of Install-Package.
<PackageReference Include="SimpleSAT" Version="1.0.1" />
For projects that support PackageReference, copy this XML node into the project file to reference the package.
paket add SimpleSAT --version 1.0.1
#r "nuget: SimpleSAT, 1.0.1"
#r directive can be used in F# Interactive and Polyglot Notebooks. Copy this into the interactive tool or source code of the script to reference the package.
// Install SimpleSAT as a Cake Addin
#addin nuget:?package=SimpleSAT&version=1.0.1

// Install SimpleSAT as a Cake Tool
#tool nuget:?package=SimpleSAT&version=1.0.1


A .Net compatible boolean satisfiability encoder


Lower level encoder

This library provides a simple interface (SimpleSAT.Encoding.SATEncoding class) for creating Boolean Satisfiability Problem (SAT) formulas. The library also provides a simple solution parser which can parse the output of a standardized SAT solver using the modern solution output format.

Higher level encoder

The library also provides a more high level encoder (SimpleSAT.Proto.ProtoEncoder class) which makes the process of creating SAT encodings simpler because the encoder automates literal indexing and auxiliary variable management. The high lever encoder is sligly less efficient because it involves the process of transforming the encoding to the afore mentioned low level encoding first (process is O(N) where N is the total length of the clauses). Slightly more memory is required as well but this is also O(N).

Debug tools

The package also contains various tools which can help you debug your encoding. For example the CNFWriter class can be used to write a "human readable" CNF file. Comments can be added to describe clauses and each literal can be assigned an arbitrary name which will appear in the readable CNF form instead of a pure integer.

The package also supports solving CNF files using a standardize SAT or MaxSAT solver (e.g. Kissat or MaxHS). You can use the SimpleSAT.SATSolver class to solve CNF files using a path to the SAT solver binary (or you can pass a process instead). The SAT solver process will then be run and it's outut is automatically parsed if the solver ran succesfully.


This package is not the most efficient encoder but the running time is dominated by the SAT solver so a slighly inefficient encoder will not cause any noticeable performance impacts. This package is good for experimenting with new encoding schemes and/or debugging encodings as well as for learning purposes for beginners.

Product Versions
.NET net6.0 net6.0-android net6.0-ios net6.0-maccatalyst net6.0-macos net6.0-tvos net6.0-windows net7.0 net7.0-android net7.0-ios net7.0-maccatalyst net7.0-macos net7.0-tvos net7.0-windows
Compatible target framework(s)
Additional computed target framework(s)
Learn more about Target Frameworks and .NET Standard.
  • net6.0

    • No dependencies.

NuGet packages

This package is not used by any NuGet packages.

GitHub repositories

This package is not used by any popular GitHub repositories.

Version Downloads Last updated
1.0.1 322 2/2/2022
1.0.0 300 2/2/2022