.NET 10.0 LINQ bindings for the Z3 theorem prover from Microsoft Research.
Based on the proof of concept by Bart De Smet which was curated into Z3.LinqBinding by Ricardo Niepel.
A number of examples are included as standalone Spectre.Console demos in demos/, each a single-file .NET app. Run the interactive launcher with dotnet run demos/menu.cs, or run any one directly, e.g. dotnet run demos/sudoku.cs; see the demos README for the full list.
Provide a solution where either X is true or Y is true, but not both (using a ValueTuple).
using (var ctx = new Z3Context())
{
var theorem = from t in ctx.NewTheorem<(bool x, bool y)>()
where t.x ^ t.y
select t;
var result = theorem.Solve();
Console.WriteLine(result);
}Solve the following system with 3 variables, with linear equalities and inequalities:
using (var ctx = new Z3Context())
{
var theorem = from t in ctx.NewTheorem<Symbols<int, int, int>>()
where t.X1 - t.X2 >= 1
where t.X1 - t.X2 <= 3
where t.X1 == (2 * t.X3) + t.X2
select t;
var result = theorem.Solve();
Console.WriteLine(result);
}In this example, we have two countries that produce crude oil which we refine into three end-products: gasoline, jet fuel, and lubricant. The crude oil from each country yields different quantities of end-products once the oil is refined:
| Saudi Arabia | Venezuela | |
|---|---|---|
| Cost | $20 / barrel | $15 / barrel |
| Max Order | 9000 barrels | 6000 barrels |
| Refining % | 30% gasolene | 40% gasolene |
| 40% jet fuel | 20% jet fuel | |
| 20% lubricant | 30% lubricant | |
| 10% waste | 10% waste |
Given we need to produce the following volume of refined end-product:
| Product | Amount (barrels) |
|---|---|
| Gasolene | 1900 |
| Jet Fuel | 1500 |
| Lubricant | 500 |
What is the most cost efficient purchase strategy of crude oil from Saudi Arabia and Venezuela?
using (var ctx = new Z3Context())
{
var theorem = from t in ctx.NewTheorem<(double sa, double vz)>()
where 0.3 * t.sa + 0.4 * t.vz >= 1900 // Gasolene
where 0.4 * t.sa + 0.2 * t.vz >= 1500 // Jet fuel
where 0.2 * t.sa + 0.3 * t.vz >= 500 // Lubricant
where 0 <= t.sa && t.sa <= 9000 // Max # barrels we can purchase
where 0 <= t.vz && t.vz <= 6000 // Max # barrels we can purchase
orderby (20.0 * t.sa) + (15.0 * t.vz) // Optimize for cost
select t;
var result = theorem.Solve();
Console.WriteLine($"SA: {result.sa} barrels (${result.sa * 20}), VZ: {result.vz} barrels (${result.vz * 15})");
}In this example, you want to minimize the cost of shipping goods from 2 different warehouses to 4 different customers. Each warehouse has a limited supply and each customer has a certain demand.
Cost of shipping ($ per product):
| Customer 1 | Customer 2 | Customer 3 | Customer 4 | |
|---|---|---|---|---|
| Warehouse 1 | $1.00 | $3.00 | $0.50 | $4.00 |
| Warehouse 2 | $2.50 | $5.00 | $1.50 | $2.50 |
Number of products shipped:
| Customer 1 | Customer 2 | Customer 3 | Customer 4 | Total shipped | Available | ||
|---|---|---|---|---|---|---|---|
| Warehouse 1 | 0 | 13,000 | 15,000 | 32,000 | 60,000 | <= | 60,000 |
| Warehouse 2 | 30,000 | 10,000 | 0 | 0 | 40,000 | <= | 80,000 |
| Total received | 30,000 | 23,000 | 15,000 | 32,000 | |||
| Ordered | 35,000 | 22,000 | 18,000 | 30,000 | |||
| Total Shipping Cost | $299,500.00 |
- The objective is to minimize the cost (Total Shipping Cost).
- The variables are the number of products to ship from each warehouse to each customer.
- The constraints are the number of products ordered and the number of products available in each warehouse.
using (var ctx = new Z3Context())
{
var theorem =
from t in ctx.NewTheorem<(double w1c1, double w1c2, double w1c3, double w1c4, double w2c1, double w2c2, double w2c3, double w2c4)>()
where t.w1c1 + t.w1c2 + t.w1c3 + t.w1c4 <= 60_000 // Warehouse 1 Product Availability
where t.w2c1 + t.w2c2 + t.w2c3 + t.w2c4 <= 80_000 // Warehouse 2 Product Availability
where t.w1c1 + t.w2c1 == 35_000 && (t.w1c1 >= 0 && t.w2c1 >= 0) // Customer 1 Orders
where t.w1c2 + t.w2c2 == 22_000 && (t.w1c2 >= 0 && t.w2c2 >= 0) // Customer 2 Orders
where t.w1c3 + t.w2c3 == 18_000 && (t.w1c3 >= 0 && t.w2c3 >= 0) // Customer 3 Orders
where t.w1c4 + t.w2c4 == 30_000 && (t.w1c4 >= 0 && t.w2c4 >= 0) // Customer 4 Orders
orderby (1.00 * t.w1c1) + (3.00 * t.w1c2) + (0.50 * t.w1c3) + (4.00 * t.w1c4) +
(2.50 * t.w2c1) + (5.00 * t.w2c2) + (1.50 * t.w2c3) + (2.50 * t.w2c4) // Optimize for Total Shipping Cost
select t;
var result = theorem.Solve();
Console.WriteLine($"| | Customer 1 | Customer 2 | Customer 3 | Customer 4 |");
Console.WriteLine($"|---------------------|------------|-------------|------------|------------|");
Console.WriteLine($"| Warehouse 1 | {result.w1c1} | {result.w1c2} | {result.w1c3} | {result.w1c4} |");
Console.WriteLine($"| Warehouse 2 | {result.w2c1} | {result.w2c2} | {result.w2c3} | {result.w2c4} |");
Console.WriteLine();
Console.WriteLine(string.Create(CultureInfo.CreateSpecificCulture("en-US"), $"Total Cost: {1.00 * result.w1c1 + 3.00 * result.w1c2 + 0.50 * result.w1c3 + 4.00 * result.w1c4 + 2.50 * result.w2c1 + 5.00 * result.w2c2 + 1.50 * result.w2c3 + 2.50 * result.w2c4:C}"));
}Solve() reports an unsatisfiable theorem by returning default. For a class environment such as
Symbols<int, int> that is null and reads correctly. For a value type - a value tuple, a struct,
a record struct - default is a fully populated instance with every symbol zero, which is also the
answer to plenty of satisfiable theorems, and it cannot even be compared against null:
using (var ctx = new Z3Context())
{
var theorem = from t in ctx.NewTheorem<(int a, int b)>()
where t.a == t.b && t.a > 4 && t.b < 2
select t;
Console.WriteLine(theorem.Solve()); // (0, 0) - and so is a theorem solved by (0, 0)
}Use TrySolve where the difference matters. It works for every environment type:
if (theorem.TrySolve(out var result))
{
Console.WriteLine($"{result.a}, {result.b}");
}
else
{
Console.WriteLine("No solution.");
}For a value-type environment, SolveOrNull() gives back a Nullable<T> instead, so the usual null
checks apply:
(int a, int b)? result = theorem.SolveOrNull();
if (result is null)
{
Console.WriteLine("No solution.");
}Both have optimisation counterparts - TryOptimize and OptimizeOrNull - and TrySolve is
available on the deferred form an orderby query returns:
var solveable = from t in ctx.NewTheorem<(int a, int b)>()
where t.a >= 5 && t.a <= 9
orderby t.a
select t;
if (solveable.TrySolve(out var cheapest)) { /* ... */ }Some theorems cannot be decided. Nonlinear integer arithmetic is undecidable in general, and a
theorem such as three integers whose cubes sum to 42 leaves Z3 searching until the process is
killed - the constraints look no more exotic than the ones above. Bound the solve with a
Timeout, or with a ResourceLimit, which counts Z3's own units of work and so is reached at the
same point on every machine:
using (var ctx = new Z3Context { Timeout = TimeSpan.FromSeconds(5) })
{
var theorem = from t in ctx.NewTheorem<Symbols<int, int, int>>()
where (t.X1 * t.X1 * t.X1) + (t.X2 * t.X2 * t.X2) + (t.X3 * t.X3 * t.X3) == 42
select t;
try
{
var result = theorem.Solve();
}
catch (TheoremUndecidedException e)
{
Console.WriteLine($"Z3 stopped: {e.Reason}"); // Z3 stopped: timeout
}
}Every solve and optimisation also takes a CancellationToken, which interrupts Z3 and throws
OperationCanceledException as usual:
using var cancellation = new CancellationTokenSource(TimeSpan.FromSeconds(5));
var result = theorem.Solve(cancellation.Token);A theorem Z3 decides within the limit is unaffected, and TrySolve returning false still means
exactly one thing: the theorem was proved to have no solution. A solve that stops without deciding
throws, so it can never be mistaken for one.
You can install the Z3.Linq NuGet Package.
Add the Z3.Linq package. No platform target is needed: Microsoft.Z3 supplies native binaries for x64 and arm64 on Windows, Linux and macOS, and the default AnyCPU resolves the right one.
Note
This applies from the next release onwards. The versions published so far depend on Microsoft.Z3 4.12.2 - the newest build on nuget.org - which ships native binaries for win-x64 and osx-x64 only. On Linux or arm64 those versions restore successfully and then throw DllNotFoundException on the first solve, so they do need an x64 platform target on Windows or macOS. Releases are paused until Z3 publishes a current build to nuget.org - see #60.
There are a number of ways in which you could contribute to this project:
- Create new examples!
- Improve the documentation.
- Report / fix bugs.
- Suggest any implementation improvements or optimizations.
- Blog about the project!
All PRs are welcome.
2009: Bart De Smet describes a prototype LINQ to Z3 binding in three blog posts:
- LINQ to Z3 - Part 1 – Exploring The Z3 Theorem Prover
- LINQ to Z3 - Part 2 – LINQ to the Unexpected
- LINQ to Z3 - Part 3 – Theorem Solving On Steroids
2010: Bart was interviewed on Channel 9 about the LINQ to Z3 concept:
2012: Bart presented LINQ to Everything at TechEd Europe 2012:
2015: Z3 was open sourced under the MIT license and the source code was moved to GitHub, where it is actively maintained.
2015: Ricardo Niepel (Microsoft) publishes the sample as Z3.LinqBinding using .NET 4.5 and Z3 binaries 4.4.0
2018: Jean-Sylvain Boige (My Intelligence Agency) adds Missionaries And Cannibals sample.
2020: Karel Frajtak adds support for fractions.
2021: Howard van Rooijen and Ian Griffiths (endjin) upgrade the project to .NET 6.0, added Optimize support via LINQ's OrderBy, ValueTuple support, demonstrate using record types, and fix nullability issues. They upgraded the solution to use Z3 NuGet package, merged in features from Jean-Sylvain Boige and Karel Frajtak forks, created archives of Bart's original blog posts and talks. They republished the project as Z3.Linq and published a NuGet package Z3.Linq.
2023: Whit Waldo upgrades the project to .NET 8.0
2026: Howard van Rooijen (endjin) upgrades the project to .NET 10.0, adopts Central Package Management, migrates the solution to the .slnx format, and moves the build to ZeroFailed.
This project is sponsored by endjin, a UK based Technology Consultancy which specializes in Data, AI, DevOps & Cloud, and is a .NET Foundation Corporate Sponsor.
We help small teams achieve big things.
We produce two free weekly newsletters:
- Azure Weekly for all things about the Microsoft Azure Platform
- Power BI Weekly for all things Power BI, Microsoft Fabric, and Azure Synapse Analytics
Keep up with everything that's going on at endjin via our blog, follow us on Twitter, YouTube or LinkedIn.
We have become the maintainers of a number of popular .NET Open Source Projects:
And we have over 50 Open Source projects of our own, spread across the following GitHub Orgs:
And the DevOps tooling we have created for managing all these projects is available on the PowerShell Gallery.
For more information about our products and services, or for commercial support of this project, please contact us.
This project has adopted a code of conduct adapted from the Contributor Covenant to clarify expected behavior in our community. This code of conduct has been adopted by many other projects. For more information see the Code of Conduct FAQ or contact hello@endjin.com with any additional questions or comments.
The IP Maturity Model is endjin's IP quality assessment framework, which we've developed over a number of years when doing due diligence assessments of 3rd party systems. We've codified the approach into a configurable set of rules, which are committed into the root of a repo, and a Azure Function HttpTrigger HTTP endpoint which can evaluate the ruleset, and render an svg badge for display in repo's readme.md.