# GitHub - endjin/Z3.Linq: LINQ bindings for the Z3 theorem prover from Microsoft...

Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.

# Z3.Linq

.NET 6.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.

## Examples

A number of examples are included in this solution, which you can run from .NET Interactive (requires Visual Studio Code) or from Visual Studio.

### Problem - 1st Order Propositional Logic

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);
}``````

### Problem - Linear Algebra

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);
}``````

### Problem - Price Optimised Oil Purchasing

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})");
}``````

### Problem - Minimizing Shipping Costs

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
1. The objective is to minimize the cost (Total Shipping Cost).
2. The variables are the number of products to ship from each warehouse to each customer.
3. 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}"));
}``````

## Getting Started

You can install the Z3.Linq NuGet Package.

### For .NET Interactive

``````#r "nuget:Z3.Linq"
``````

Then add the following using statements:

``````using System;
using Z3.Linq;``````

Then you can copy any of the above samples.

### For Visual Studio

Add the `Z3.Linq` package. Configure your application to target x64 platform. This is a requirement as `Z3.Linq` uses the Microsoft.Z3 package.

## Contributing

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.

All PRs are welcome.

## History

2009: Bart De Smet describes a prototype LINQ to Z3 binding in three blog posts:

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`

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, created a new .NET Interactive Notebook of samples, and published a NuGet package Z3.Linq.