diff --git a/README.md b/README.md index dc56aac..e020980 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ Based on the proof of concept by [Bart De Smet](https://github.com/bartdesmet) w ## Examples -A number of examples are included in this solution, which you can run [from .NET Interactive](examples/z3-problems.dib) (requires [Visual Studio Code](https://code.visualstudio.com/)) or [from Visual Studio](solutions/Z3.Linq.Demo/Program.cs). +A number of examples are included as standalone [Spectre.Console](https://spectreconsole.net/) demos in [`demos/`](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](demos/README.md) for the full list. ### Problem - 1st Order Propositional Logic @@ -239,20 +239,6 @@ throws, so it can never be mistaken for one. You can install the [Z3.Linq NuGet Package](https://www.nuget.org/packages/Z3.Linq/). -### For Polyglot Notebooks - -Add the package: -``` -#r "nuget:Z3.Linq" -``` -Then add the following using statements: - -```csharp -using System; -using Z3.Linq; -``` -Then you can copy any of the above samples. - ### For Visual Studio 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. @@ -296,7 +282,7 @@ All PRs are welcome. 2020: [Karel Frajtak](https://github.com/kfrajtak) adds [support for fractions](https://github.com/kfrajtak/Z3.LinqBinding). -2021: [Howard van Rooijen](https://github.com/HowardvanRooijen) and [Ian Griffiths](https://github.com/idg10) ([endjin](https://github.com/endjin)) upgrade the project to `.NET 6.0`, added `Optimize` support via LINQ's `OrderBy`, [ValueTuple](https://docs.microsoft.com/en-us/dotnet/api/system.valuetuple?view=net-6.0) support, demonstrate using `record` types, and fix nullability issues. They upgraded the solution to use [Z3 NuGet package](https://www.nuget.org/packages/Microsoft.Z3.x64/), merged in features from [Jean-Sylvain Boige](https://github.com/jsboige) and [Karel Frajtak](https://github.com/kfrajtak) forks, created archives of Bart's original blog posts and talks. They republished the project as [Z3.Linq](https://github.com/endjin/Z3.Linq), created a new [Polyglot Notebook](https://github.com/dotnet/interactive) of [samples](examples/z3-problems.dib), and published a NuGet package [Z3.Linq](https://www.nuget.org/packages/Z3.Linq/). +2021: [Howard van Rooijen](https://github.com/HowardvanRooijen) and [Ian Griffiths](https://github.com/idg10) ([endjin](https://github.com/endjin)) upgrade the project to `.NET 6.0`, added `Optimize` support via LINQ's `OrderBy`, [ValueTuple](https://docs.microsoft.com/en-us/dotnet/api/system.valuetuple?view=net-6.0) support, demonstrate using `record` types, and fix nullability issues. They upgraded the solution to use [Z3 NuGet package](https://www.nuget.org/packages/Microsoft.Z3.x64/), merged in features from [Jean-Sylvain Boige](https://github.com/jsboige) and [Karel Frajtak](https://github.com/kfrajtak) forks, created archives of Bart's original blog posts and talks. They republished the project as [Z3.Linq](https://github.com/endjin/Z3.Linq) and published a NuGet package [Z3.Linq](https://www.nuget.org/packages/Z3.Linq/). 2023: [Whit Waldo](https://github.com/WhitWaldo) upgrades the project to `.NET 8.0` diff --git a/demos/README.md b/demos/README.md new file mode 100644 index 0000000..6a3953e --- /dev/null +++ b/demos/README.md @@ -0,0 +1,44 @@ +# Z3.Linq demos + +A set of standalone [Spectre.Console](https://spectreconsole.net/) demos for `Z3.Linq`, each a +single-file [.NET file-based app](https://learn.microsoft.com/dotnet/core/whats-new/dotnet-10#file-based-apps). +No project, no solution entry - just run the file: + +```bash +dotnet run demos/sudoku.cs +``` + +The first run of a file restores its packages and builds it; later runs are fast. Each file +declares its own dependencies at the top (`#:package Spectre.Console`, `#:project ...` to the +`Z3.Linq` and `Z3.Linq.Examples` projects in [`../solutions`](../solutions)), so they build against +your local source. + +## The demos + +| File | Problem | +|------|---------| +| [`menu.cs`](menu.cs) | An interactive launcher - pick a demo from a Spectre menu and it runs the others. | +| [`river-crossing.cs`](river-crossing.cs) | Missionaries & Cannibals, showing `Solve` (any plan) against `Optimize`/`orderby` (the shortest plan). | +| [`sudoku.cs`](sudoku.cs) | Two Sudoku puzzles solved on a rendered 9x9 grid, clues driven through expression-tree constraints. | +| [`boolean-logic.cs`](boolean-logic.cs) | `x XOR y` over an anonymous type, a value tuple, and a record - the same theorem, three environment shapes. | +| [`linear-systems.cs`](linear-systems.cs) | Small integer constraint systems, including Bart De Smet's TechEd Europe 2012 example. | +| [`oil-purchase.cs`](oil-purchase.cs) | A least-cost linear program (`orderby` minimises the bill). | +| [`warehouse.cs`](warehouse.cs) | Least-cost shipping across two warehouses to four customers. | + +## Running everything + +```bash +# interactive launcher +dotnet run demos/menu.cs + +# or one at a time +dotnet run demos/river-crossing.cs +dotnet run demos/sudoku.cs +dotnet run demos/boolean-logic.cs +dotnet run demos/linear-systems.cs +dotnet run demos/oil-purchase.cs +dotnet run demos/warehouse.cs +``` + +Output is styled when run in a terminal and degrades to plain text when redirected (piped to a file +or another program), so the demos are safe to capture in scripts. diff --git a/demos/boolean-logic.cs b/demos/boolean-logic.cs new file mode 100644 index 0000000..2f08bfc --- /dev/null +++ b/demos/boolean-logic.cs @@ -0,0 +1,76 @@ +#:project ../solutions/Z3.Linq/Z3.Linq.csproj +#:project ../solutions/Z3.Linq.Examples/Z3.Linq.Examples.csproj +#:package Spectre.Console@0.57.2 + +// The same Boolean theorem - find x, y with x XOR y true - expressed three ways: an anonymous type, +// a value tuple, and a record. Shows that the environment type is just a shape Z3.Linq marshals to. +// +// dotnet run demos/boolean-logic.cs + +using System.Diagnostics; + +using Spectre.Console; + +using Z3.Linq; +using Z3.Linq.Examples; + +AnsiConsole.Write(new FigletText("Boolean Logic").Color(Color.Aqua).Centered()); +AnsiConsole.Write(new Rule("[aqua]x XOR y[/]")); +AnsiConsole.WriteLine(); + +AnsiConsole.Write(new Panel( + "Find Boolean [aqua]x[/] and [aqua]y[/] such that [yellow]x ^ y[/] holds - the one theorem written\n" + + "over three different environment types. Z3 solves each the same way.") + .Header("[white]The problem[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey)); +AnsiConsole.WriteLine(); + +var table = new Table().Border(TableBorder.Rounded).BorderColor(Color.Grey) + .AddColumn("[white]Environment type[/]") + .AddColumn(new TableColumn("[white]x[/]").Centered()) + .AddColumn(new TableColumn("[white]y[/]").Centered()) + .AddColumn(new TableColumn("[white]x ^ y[/]").Centered()) + .AddColumn(new TableColumn("[white]Time[/]").RightAligned()); + +using (var ctx = new Z3Context()) +{ + var theorem = from t in ctx.NewTheorem(new { x = default(bool), y = default(bool) }) + where t.x ^ t.y + select t; + // Solve() returns T?, null only when unsatisfiable - which x ^ y never is. The ! is needed + // for the reference-type environments (this and the record below); the value tuple is not null. + var (r, ms) = Time(() => theorem.Solve()!); + table.AddRow("[grey]anonymous type[/]", Bool(r.x), Bool(r.y), Bool(r.x ^ r.y), Ms(ms)); +} + +using (var ctx = new Z3Context()) +{ + var theorem = from t in ctx.NewTheorem<(bool x, bool y)>() + where t.x ^ t.y + select t; + var (r, ms) = Time(() => theorem.Solve()); + table.AddRow("[grey]value tuple[/]", Bool(r.x), Bool(r.y), Bool(r.x ^ r.y), Ms(ms)); +} + +using (var ctx = new Z3Context()) +{ + var theorem = from t in ctx.NewTheorem(new RecordTheorem()) + where t.X ^ t.Y + select t; + var (r, ms) = Time(() => theorem.Solve()!); + table.AddRow("[grey]record[/]", Bool(r.X), Bool(r.Y), Bool(r.X ^ r.Y), Ms(ms)); +} + +AnsiConsole.Write(table); +AnsiConsole.MarkupLine("[grey] Each row is an independent solve; XOR has two solutions, so Z3 may pick either.[/]"); + +static string Bool(bool b) => b ? "[green]true[/]" : "[red]false[/]"; + +static string Ms(double ms) => $"[grey]{ms:F1} ms[/]"; + +static (T Result, double Ms) Time(Func solve) +{ + var sw = Stopwatch.StartNew(); + T result = solve(); + sw.Stop(); + return (result, sw.Elapsed.TotalMilliseconds); +} diff --git a/demos/linear-systems.cs b/demos/linear-systems.cs new file mode 100644 index 0000000..ed326f6 --- /dev/null +++ b/demos/linear-systems.cs @@ -0,0 +1,94 @@ +#:project ../solutions/Z3.Linq/Z3.Linq.csproj +#:package Spectre.Console@0.57.2 + +// Small systems of linear integer constraints, solved as Z3 theorems and rendered with +// Spectre.Console. Includes Bart De Smet's example from TechEd Europe 2012, shown over both a +// Symbols environment and an equivalent value tuple. +// +// dotnet run demos/linear-systems.cs + +using System.Diagnostics; + +using Spectre.Console; + +using Z3.Linq; + +AnsiConsole.Write(new FigletText("Linear Systems").Color(Color.Yellow).Centered()); +AnsiConsole.Write(new Rule("[yellow]integer constraint solving[/]")); +AnsiConsole.WriteLine(); + +// Bart's TechEd Europe 2012 example, over Symbols. +using (var ctx = new Z3Context()) +{ + var theorem = from t in ctx.NewTheorem>() + where t.X1 - t.X2 >= 1 + where t.X1 - t.X2 <= 3 + where t.X1 == (2 * t.X3) + t.X2 + select t; + + // Solve() returns T?, null only when unsatisfiable; ! since Symbols<...> is a reference type. + var (r, ms) = Time(() => theorem.Solve()!); + Section("Bart's example (TechEd Europe 2012)", + ["x1 - x2 >= 1", "x1 - x2 <= 3", "x1 == 2*x3 + x2"], + [("x1", r.X1), ("x2", r.X2), ("x3", r.X3)], ms); +} + +// The same system over a value tuple. +using (var ctx = new Z3Context()) +{ + var theorem = from t in ctx.NewTheorem<(int x, int y, int z)>() + where t.x - t.y >= 1 + where t.x - t.y <= 3 + where t.x == (2 * t.z) + t.y + select t; + + var (r, ms) = Time(() => theorem.Solve()); + Section("The same system over a value tuple", + ["x - y >= 1", "x - y <= 3", "x == 2*z + y"], + [("x", r.x), ("y", r.y), ("z", r.z)], ms); +} + +// A Symbols example with an inequality and a distinctness constraint. +using (var ctx = new Z3Context()) +{ + var theorem = from t in ctx.NewTheorem>() + where t.X1 < t.X2 + 1 + where t.X1 > 2 + where t.X1 != t.X2 + select t; + + var (r, ms) = Time(() => theorem.Solve()!); + Section("A Symbols example", + ["x1 < x2 + 1", "x1 > 2", "x1 != x2"], + [("x1", r.X1), ("x2", r.X2)], ms); +} + +void Section(string title, string[] constraints, (string Name, int Value)[] solution, double ms) +{ + AnsiConsole.Write(new Rule($"[yellow]{title}[/]").LeftJustified()); + + var constraintList = new Panel(string.Join("\n", constraints.Select(c => $"[white]{c}[/]"))) + .Header("[white]Constraints[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey); + + var table = new Table().Border(TableBorder.Rounded).BorderColor(Color.Yellow) + .AddColumn(new TableColumn("[white]Symbol[/]").Centered()) + .AddColumn(new TableColumn("[white]Value[/]").Centered()); + foreach (var (name, value) in solution) + { + table.AddRow($"[yellow]{name}[/]", $"[white]{value}[/]"); + } + + var layout = new Grid().AddColumn().AddColumn(); + layout.AddRow(constraintList, new Panel(table).Header("[white]Solution[/]").Border(BoxBorder.None)); + AnsiConsole.Write(layout); + AnsiConsole.MarkupLine($"[grey] Solved in {ms:F1} ms[/]"); + AnsiConsole.WriteLine(); +} + +static (T Result, double Ms) Time(Func solve) +{ + var sw = Stopwatch.StartNew(); + T result = solve(); + sw.Stop(); + return (result, sw.Elapsed.TotalMilliseconds); +} diff --git a/demos/menu.cs b/demos/menu.cs new file mode 100644 index 0000000..6e2b0a2 --- /dev/null +++ b/demos/menu.cs @@ -0,0 +1,75 @@ +#:package Spectre.Console@0.57.2 + +// An interactive launcher for the Z3.Linq demos. Presents a Spectre.Console menu and runs the +// chosen demo as its own file-based app (`dotnet run demos/.cs`). +// +// dotnet run demos/menu.cs + +using System.Diagnostics; + +using Spectre.Console; + +var demos = new (string Name, string File, string Blurb)[] +{ + ("River crossing", "river-crossing.cs", "Missionaries & Cannibals - Solve, Optimize and orderby"), + ("Sudoku", "sudoku.cs", "Two puzzles solved on a 9x9 grid"), + ("Boolean logic", "boolean-logic.cs", "x XOR y over an anonymous type, a tuple and a record"), + ("Linear systems", "linear-systems.cs", "Integer constraint systems, incl. Bart's TechEd example"), + ("Oil purchase", "oil-purchase.cs", "A least-cost linear program"), + ("Warehouse logistics", "warehouse.cs", "Least-cost shipping across two warehouses"), +}; + +// Run from the repo root (`dotnet run demos/menu.cs`) or from within demos/. +string dir = File.Exists("river-crossing.cs") ? "." : "demos"; + +AnsiConsole.Write(new FigletText("Z3.Linq").Color(Color.Aqua).Centered()); +AnsiConsole.Write(new Rule("[aqua]demos[/]")); +AnsiConsole.WriteLine(); + +const string quit = "Quit"; + +while (true) +{ + var choice = AnsiConsole.Prompt( + new SelectionPrompt() + .Title("Choose a [green]demo[/] to run:") + .PageSize(10) + .UseConverter(name => name == quit + ? "[grey]Quit[/]" + : $"{name} [grey]- {demos.First(d => d.Name == name).Blurb}[/]") + .AddChoices([.. demos.Select(d => d.Name), quit])); + + if (choice == quit) + { + break; + } + + var demo = demos.First(d => d.Name == choice); + + AnsiConsole.WriteLine(); + AnsiConsole.Write(new Rule($"[green]{Markup.Escape(demo.Name)}[/]")); + + var start = new ProcessStartInfo("dotnet") { UseShellExecute = false }; + start.ArgumentList.Add("run"); + start.ArgumentList.Add(Path.Combine(dir, demo.File)); + + try + { + using var process = Process.Start(start); + process!.WaitForExit(); + } + catch (Exception ex) + { + AnsiConsole.WriteException(ex, ExceptionFormats.ShortenPaths); + } + + AnsiConsole.WriteLine(); + if (!AnsiConsole.Confirm("Run [green]another[/] demo?")) + { + break; + } + + AnsiConsole.WriteLine(); +} + +AnsiConsole.MarkupLine("[grey]Bye![/]"); diff --git a/demos/oil-purchase.cs b/demos/oil-purchase.cs new file mode 100644 index 0000000..18032d7 --- /dev/null +++ b/demos/oil-purchase.cs @@ -0,0 +1,60 @@ +#:project ../solutions/Z3.Linq/Z3.Linq.csproj +#:package Spectre.Console@0.57.2 + +// The classic oil-purchase linear program, solved as a Z3 theorem and rendered with +// Spectre.Console. Buy crude from Saudi Arabia and Venezuela to meet minimum yields of three +// products at the least cost. `orderby` asks Z3 to minimise total spend. +// +// dotnet run demos/oil-purchase.cs + +using System.Diagnostics; +using System.Globalization; + +using Spectre.Console; + +using Z3.Linq; + +var money = CultureInfo.CreateSpecificCulture("en-US"); + +AnsiConsole.Write(new FigletText("Oil Purchase").Color(Color.Orange1).Centered()); +AnsiConsole.Write(new Rule("[orange1]a least-cost linear program[/]")); +AnsiConsole.WriteLine(); + +AnsiConsole.Write(new Panel( + "Each barrel of [orange1]Saudi[/] crude yields 0.3 gasoline / 0.4 jet fuel / 0.2 lubricant;\n" + + "each [orange1]Venezuelan[/] barrel yields 0.4 / 0.2 / 0.3. Demand is at least [white]1900[/] / [white]1500[/] / [white]500[/].\n" + + "Saudi is [green]$20[/]/barrel, Venezuela [green]$15[/] - [italic]orderby[/] minimises the total bill.") + .Header("[white]The problem[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey)); +AnsiConsole.WriteLine(); + +using var ctx = new Z3Context(); +var solveable = from t in ctx.NewTheorem<(double vz, double sa)>() + where 0.3 * t.sa + 0.4 * t.vz >= 1900 + where 0.4 * t.sa + 0.2 * t.vz >= 1500 + where 0.2 * t.sa + 0.3 * t.vz >= 500 + where 0 <= t.sa && t.sa <= 9000 + where 0 <= t.vz && t.vz <= 6000 + orderby (20.0 * t.sa) + (15.0 * t.vz) + select t; + +(double vz, double sa) result = default; +var sw = Stopwatch.StartNew(); +AnsiConsole.Status().Spinner(Spinner.Known.Dots).SpinnerStyle(Style.Parse("orange1")) + .Start("[orange1]Optimising...[/]", _ => result = solveable.Solve()); +sw.Stop(); + +double saCost = result.sa * 20; +double vzCost = result.vz * 15; + +var table = new Table().Border(TableBorder.Rounded).BorderColor(Color.Orange1) + .Title("[orange1]Cheapest purchase[/]") + .AddColumn("[white]Source[/]") + .AddColumn(new TableColumn("[white]Barrels[/]").RightAligned()) + .AddColumn(new TableColumn("[white]Cost[/]").RightAligned()); +table.AddRow("Saudi Arabia", $"{result.sa:N0}", $"[green]{saCost.ToString("C", money)}[/]"); +table.AddRow("Venezuela", $"{result.vz:N0}", $"[green]{vzCost.ToString("C", money)}[/]"); +table.AddEmptyRow(); +table.AddRow("[white]Total[/]", string.Empty, $"[bold green]{(saCost + vzCost).ToString("C", money)}[/]"); + +AnsiConsole.Write(table); +AnsiConsole.MarkupLine($"[grey] Optimised in {sw.Elapsed.TotalMilliseconds:F1} ms[/]"); diff --git a/demos/river-crossing.cs b/demos/river-crossing.cs new file mode 100644 index 0000000..0a14ea4 --- /dev/null +++ b/demos/river-crossing.cs @@ -0,0 +1,114 @@ +#:project ../solutions/Z3.Linq/Z3.Linq.csproj +#:project ../solutions/Z3.Linq.Examples/Z3.Linq.Examples.csproj +#:package Spectre.Console@0.57.2 + +// The Missionaries & Cannibals river-crossing puzzle, solved as a Z3 theorem and rendered with +// Spectre.Console. Three missionaries and three cannibals must cross a river in a two-person boat, +// and the missionaries must never be outnumbered on either bank. Z3 produces the sequence of moves. +// +// dotnet run demos/river-crossing.cs + +using System.Diagnostics; + +using Spectre.Console; + +using Z3.Linq; +using Z3.Linq.Examples.RiverCrossing; + +AnsiConsole.Write(new FigletText("River Crossing").Color(Color.DodgerBlue1).Centered()); +AnsiConsole.Write(new Rule("[dodgerblue1]Missionaries & Cannibals[/]")); +AnsiConsole.WriteLine(); + +AnsiConsole.Write(new Panel( + "[white]3[/] missionaries and [white]3[/] cannibals must cross a river in a boat that holds [white]2[/].\n" + + "On neither bank may missionaries be [red]outnumbered[/] by cannibals, and the boat cannot cross empty.\n" + + "Z3 is asked only for [italic]a[/] plan by [green]Solve[/], and for the [italic]shortest[/] plan by [green]Optimize[/] and [green]orderby[/].") + .Header("[white]The problem[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey)); +AnsiConsole.WriteLine(); + +using var ctx = new Z3Context(); +var theorem = from t in MissionariesAndCannibals.Create(ctx, 50) + where t.MissionaryAndCannibalCount == 3 + where t.SizeBoat == 2 + select t; + +// Solve(): any valid plan. +MissionariesAndCannibals? plan = null; +var solveTime = Time(() => plan = theorem.Solve()); + +if (plan is null) +{ + AnsiConsole.MarkupLine("[red]No solution found.[/]"); + return; +} + +AnsiConsole.Write(BuildPlan(plan)); +AnsiConsole.WriteLine(); + +// Optimize() and orderby: the shortest plan. +MissionariesAndCannibals? optimized = null; +var optimizeTime = Time(() => optimized = theorem.Optimize(Optimization.Minimize, t => t.Length)); + +MissionariesAndCannibals? ordered = null; +var orderByTime = Time(() => ordered = (from t in theorem orderby t.Length select t).Solve()); + +var compare = new Table().Border(TableBorder.Rounded).BorderColor(Color.Grey) + .AddColumn("[white]Method[/]") + .AddColumn(new TableColumn("[white]Steps[/]").Centered()) + .AddColumn(new TableColumn("[white]Time[/]").RightAligned()); +compare.AddRow("[green]Solve[/] - any plan", plan.Length.ToString(), $"[grey]{solveTime:F0} ms[/]"); +compare.AddRow("[green]Optimize[/] - minimise Length", (optimized?.Length)?.ToString() ?? "-", $"[grey]{optimizeTime:F0} ms[/]"); +compare.AddRow("[green]orderby[/] - minimise Length", (ordered?.Length)?.ToString() ?? "-", $"[grey]{orderByTime:F0} ms[/]"); +AnsiConsole.Write(new Panel(compare).Header("[white]Solve vs. optimise[/]").Border(BoxBorder.None)); + +// Renders the crossing plan as a table: bank populations at each step, and the move between them. +static Table BuildPlan(MissionariesAndCannibals plan) +{ + int n = plan.MissionaryAndCannibalCount; + + var table = new Table().Border(TableBorder.Rounded).BorderColor(Color.DodgerBlue1) + .Title("[dodgerblue1]The crossing[/]") + .AddColumn(new TableColumn("[white]Step[/]").Centered()) + .AddColumn("[white]Start bank[/]") + .AddColumn(new TableColumn("[white]Boat[/]").Centered()) + .AddColumn("[white]Far bank[/]"); + + for (int i = 0; i < plan.Length; i++) + { + int m = plan.Missionaries[i]; + int c = plan.Cannibals[i]; + string start = Bank(m, c); + string far = Bank(n - m, n - c); + string boat = Move(plan, i); + table.AddRow((i + 1).ToString(), start, boat, far); + } + + return table; +} + +static string Bank(int missionaries, int cannibals) => + $"[yellow]{new string('M', missionaries)}[/][red]{new string('C', cannibals)}[/]" + + (missionaries + cannibals == 0 ? "[grey](empty)[/]" : $" [grey]({missionaries}M {cannibals}C)[/]"); + +static string Move(MissionariesAndCannibals plan, int i) +{ + if (i >= plan.Length - 1) + { + return "[green]done[/]"; + } + + // Even steps send the boat to the far bank; odd steps bring it back. + int dm = Math.Abs(plan.Missionaries[i + 1] - plan.Missionaries[i]); + int dc = Math.Abs(plan.Cannibals[i + 1] - plan.Cannibals[i]); + string load = $"[yellow]{new string('M', dm)}[/][red]{new string('C', dc)}[/]"; + return i % 2 == 0 ? $"{load} [dodgerblue1]-->[/]" : $"[dodgerblue1]<--[/] {load}"; +} + +static double Time(Action action) +{ + var sw = Stopwatch.StartNew(); + AnsiConsole.Status().Spinner(Spinner.Known.Dots).SpinnerStyle(Style.Parse("dodgerblue1")) + .Start("[dodgerblue1]Solving...[/]", _ => action()); + sw.Stop(); + return sw.Elapsed.TotalMilliseconds; +} diff --git a/demos/sudoku.cs b/demos/sudoku.cs new file mode 100644 index 0000000..bc62e76 --- /dev/null +++ b/demos/sudoku.cs @@ -0,0 +1,153 @@ +#:project ../solutions/Z3.Linq/Z3.Linq.csproj +#:project ../solutions/Z3.Linq.Examples/Z3.Linq.Examples.csproj +#:package Spectre.Console@0.57.2 + +// Sudoku solved as a Z3 theorem, rendered with Spectre.Console. +// +// SudokuTheorem.Create(ctx) supplies the rules (row/column/box all-distinct, 1..9); this demo +// adds the clues of a specific puzzle and asks Z3 for the unique completion. The clues drive both +// the constraints and the printed grid, so there is one source of truth for each puzzle. +// +// dotnet run demos/sudoku.cs + +using System.Diagnostics; +using System.Linq.Expressions; + +using Spectre.Console; + +using Z3.Linq; +using Z3.Linq.Examples.Sudoku; + +AnsiConsole.Write(new FigletText("Sudoku").Color(Color.Green).Centered()); +AnsiConsole.Write(new Rule("[green]solved as a Z3 theorem[/]")); +AnsiConsole.WriteLine(); + +// 0 = blank. Two well-known puzzles. +int[,] easy = +{ + { 0, 0, 2, 0, 0, 1, 0, 6, 0 }, + { 0, 0, 7, 0, 0, 4, 0, 0, 0 }, + { 5, 0, 0, 0, 0, 0, 9, 0, 0 }, + { 0, 1, 0, 3, 0, 0, 0, 0, 0 }, + { 8, 0, 0, 0, 5, 0, 0, 0, 4 }, + { 0, 0, 0, 0, 0, 6, 0, 2, 0 }, + { 0, 0, 6, 0, 0, 0, 0, 0, 7 }, + { 0, 0, 0, 8, 0, 0, 3, 0, 0 }, + { 0, 4, 0, 9, 0, 0, 2, 0, 0 }, +}; + +int[,] hard = +{ + { 0, 0, 0, 2, 6, 0, 7, 0, 1 }, + { 6, 8, 0, 0, 7, 0, 0, 9, 0 }, + { 1, 9, 0, 0, 0, 4, 5, 0, 0 }, + { 8, 2, 0, 1, 0, 0, 0, 4, 0 }, + { 0, 0, 4, 6, 0, 2, 9, 0, 0 }, + { 0, 5, 0, 0, 0, 3, 0, 2, 8 }, + { 0, 0, 9, 3, 0, 0, 0, 7, 4 }, + { 0, 4, 0, 0, 5, 0, 0, 3, 6 }, + { 7, 0, 3, 0, 1, 8, 0, 0, 0 }, +}; + +Solve("Easy", easy); +AnsiConsole.WriteLine(); +Solve("Hard (arizona.edu)", hard); + +void Solve(string name, int[,] clues) +{ + AnsiConsole.Write(new Rule($"[green]{name}[/]").LeftJustified()); + + using var ctx = new Z3Context(); + var theorem = WithClues(SudokuTheorem.Create(ctx), clues); + + SudokuTable? solution = null; + var sw = Stopwatch.StartNew(); + AnsiConsole.Status() + .Spinner(Spinner.Known.Dots) + .SpinnerStyle(Style.Parse("green")) + .Start("[green]Solving...[/]", _ => solution = theorem.Solve()); + sw.Stop(); + + if (solution is null) + { + AnsiConsole.MarkupLine("[red]No solution - the clues are contradictory.[/]"); + return; + } + + var puzzle = new Panel(Grid((r, c) => clues[r, c], (r, c) => clues[r, c] != 0)) + .Header("[grey]Puzzle[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey); + + var solved = new Panel(Grid((r, c) => Cell(solution, r, c), (r, c) => clues[r, c] != 0)) + .Header("[green]Solution[/]").Border(BoxBorder.Rounded).BorderColor(Color.Green); + + var grid = new Grid().AddColumn().AddColumn(); + grid.AddRow(puzzle, solved); + AnsiConsole.Write(grid); + AnsiConsole.MarkupLine($"[grey] Clues in [white]white[/], values Z3 derived in [green]green[/] - solved in {sw.Elapsed.TotalMilliseconds:F0} ms[/]"); +} + +// Adds one `t.Cell{r}{c} == v` constraint per clue, built as an expression tree so the puzzle +// array is the single source of truth. +static Theorem WithClues(Theorem theorem, int[,] clues) +{ + var t = Expression.Parameter(typeof(SudokuTable), "t"); + + for (int row = 1; row <= 9; row++) + { + for (int col = 1; col <= 9; col++) + { + int value = clues[row - 1, col - 1]; + if (value == 0) + { + continue; + } + + var body = Expression.Equal( + Expression.Property(t, $"Cell{row}{col}"), + Expression.Constant(value)); + + theorem = theorem.Where(Expression.Lambda>(body, t)); + } + } + + return theorem; +} + +static int Cell(SudokuTable table, int row, int col) => + (int)typeof(SudokuTable).GetProperty($"Cell{row + 1}{col + 1}")!.GetValue(table)!; + +// A 9x9 markup grid with heavy 3x3 box separators. `cell`/`isClue` are 0-based. +static string Grid(Func cell, Func isClue) +{ + const string top = "┌───────┬───────┬───────┐"; + const string mid = "├───────┼───────┼───────┤"; + const string bot = "└───────┴───────┴───────┘"; + + var sb = new System.Text.StringBuilder(); + sb.AppendLine(top); + for (int r = 0; r < 9; r++) + { + sb.Append('│'); + for (int c = 0; c < 9; c++) + { + int v = cell(r, c); + string glyph = v == 0 + ? "[grey].[/]" + : isClue(r, c) ? $"[white bold]{v}[/]" : $"[green]{v}[/]"; + sb.Append(' ').Append(glyph); + if (c % 3 == 2) + { + sb.Append(" │"); + } + } + + sb.AppendLine(); + if (r is 2 or 5) + { + sb.AppendLine(mid); + } + } + + sb.Append(bot); + return sb.ToString(); +} diff --git a/demos/warehouse.cs b/demos/warehouse.cs new file mode 100644 index 0000000..79fe24a --- /dev/null +++ b/demos/warehouse.cs @@ -0,0 +1,66 @@ +#:project ../solutions/Z3.Linq/Z3.Linq.csproj +#:package Spectre.Console@0.57.2 + +// A warehouse-logistics linear program, solved as a Z3 theorem and rendered with Spectre.Console. +// Two warehouses ship a product to four customers within stock limits and exact orders; `orderby` +// minimises the total shipping cost. +// +// dotnet run demos/warehouse.cs + +using System.Diagnostics; +using System.Globalization; + +using Spectre.Console; + +using Z3.Linq; + +var money = CultureInfo.CreateSpecificCulture("en-US"); + +AnsiConsole.Write(new FigletText("Warehouse").Color(Color.MediumPurple).Centered()); +AnsiConsole.Write(new Rule("[mediumpurple]least-cost shipping[/]")); +AnsiConsole.WriteLine(); + +AnsiConsole.Write(new Panel( + "Warehouse 1 holds up to [white]60,000[/] units, Warehouse 2 up to [white]80,000[/]. Four customers order\n" + + "[white]35,000[/] / [white]22,000[/] / [white]18,000[/] / [white]30,000[/] exactly. Per-unit shipping cost varies by lane -\n" + + "[italic]orderby[/] finds the assignment with the lowest total cost.") + .Header("[white]The problem[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey)); +AnsiConsole.WriteLine(); + +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 availability + where t.w2c1 + t.w2c2 + t.w2c3 + t.w2c4 <= 80_000 // Warehouse 2 availability + where t.w1c1 + t.w2c1 == 35_000 && t.w1c1 >= 0 && t.w2c1 >= 0 // Customer 1 order + where t.w1c2 + t.w2c2 == 22_000 && t.w1c2 >= 0 && t.w2c2 >= 0 // Customer 2 order + where t.w1c3 + t.w2c3 == 18_000 && t.w1c3 >= 0 && t.w2c3 >= 0 // Customer 3 order + where t.w1c4 + t.w2c4 == 30_000 && t.w1c4 >= 0 && t.w2c4 >= 0 // Customer 4 order + 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) // Total shipping cost + select t; + +(double w1c1, double w1c2, double w1c3, double w1c4, double w2c1, double w2c2, double w2c3, double w2c4) r = default; +var sw = Stopwatch.StartNew(); +AnsiConsole.Status().Spinner(Spinner.Known.Dots).SpinnerStyle(Style.Parse("mediumpurple")) + .Start("[mediumpurple]Optimising...[/]", _ => r = theorem.Solve()); +sw.Stop(); + +double total = (1.00 * r.w1c1) + (3.00 * r.w1c2) + (0.50 * r.w1c3) + (4.00 * r.w1c4) + + (2.50 * r.w2c1) + (5.00 * r.w2c2) + (1.50 * r.w2c3) + (2.50 * r.w2c4); + +var table = new Table().Border(TableBorder.Rounded).BorderColor(Color.MediumPurple) + .Title("[mediumpurple]Units shipped[/]") + .AddColumn("[white]From \\ To[/]") + .AddColumn(new TableColumn("[white]Customer 1[/]").RightAligned()) + .AddColumn(new TableColumn("[white]Customer 2[/]").RightAligned()) + .AddColumn(new TableColumn("[white]Customer 3[/]").RightAligned()) + .AddColumn(new TableColumn("[white]Customer 4[/]").RightAligned()); +table.AddRow("[white]Warehouse 1[/]", Units(r.w1c1), Units(r.w1c2), Units(r.w1c3), Units(r.w1c4)); +table.AddRow("[white]Warehouse 2[/]", Units(r.w2c1), Units(r.w2c2), Units(r.w2c3), Units(r.w2c4)); + +AnsiConsole.Write(table); +AnsiConsole.MarkupLine($"[white] Total shipping cost:[/] [bold green]{total.ToString("C", money)}[/]"); +AnsiConsole.MarkupLine($"[grey] Optimised in {sw.Elapsed.TotalMilliseconds:F1} ms[/]"); + +static string Units(double value) => value <= 0 ? "[grey]-[/]" : $"[mediumpurple]{value:N0}[/]"; diff --git a/examples/z3-problems.dib b/examples/z3-problems.dib deleted file mode 100644 index c01b6b1..0000000 --- a/examples/z3-problems.dib +++ /dev/null @@ -1,420 +0,0 @@ -#!meta - -{"kernelInfo":{"defaultKernelName":"csharp","items":[{"aliases":[],"name":"csharp"}]}} - -#!markdown - -If you want to run this locally, you need to build the solution in Debug mode and then reference the binaries: - -#!csharp - -#r "..\solutions\Z3.Linq\bin\Debug\net10.0\Z3.Linq.dll" -#r "..\solutions\Z3.Linq.Examples\bin\Debug\net10.0\Z3.Linq.Examples.dll" -#r "nuget:Microsoft.Z3,*-*" -#r "nuget:MiaPlaza.ExpressionUtils,*-*" - -#!markdown - -Or you can simply use the public NuGet packages: - -#!csharp - -#r "nuget:Z3.Linq,*-*" -#r "nuget:Z3.Linq.Examples,*-*" - -#!markdown - -Import the required namespaces: - -#!csharp - -using System; -using System.Diagnostics; -using System.Globalization; - -using Z3.Linq; -using Z3.Linq.Examples; -using Z3.Linq.Examples.RiverCrossing; -using Z3.Linq.Examples.Sudoku; - -#!markdown - -## Problem 1 - 1st Order Propositional Logic - -Provide a solution where either X is true or Y is true (but not both). - -#!csharp - -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); -} - -#!markdown - -## Problem 2 - Linear Algebra - -Solve the following system with 3 variables, with linear equalities and inequalities. - -$$ -x_1 - x_2 \ge 1 -\\ -x_1 - x_2 \le 3 -\\ -x_1 = 2x_3 + x_2 -$$ - -#!csharp - -using (var ctx = new Z3Context()) -{ - var theorem = from t in ctx.NewTheorem>() - 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); -} - -#!markdown - -# Problem 3 - Sudoku - -How would you solve the following Sudoku Puzzle? - -| | | | 2 | 6 | | 7 | | 1 | -|---|---|---|---|---|---|---|---|---| -| 6 | 8 | | | 7 | | | 9 | | -| 1 | 9 | | | | 4 | 5 | | | -| 8 | 2 | | 1 | | | | 4 | | -| | | 4 | 6 | | 2 | 9 | | | -| | 5 | | | | 3 | | 2 | 8 | -| | | 9 | 3 | | | | 7 | 4 | -| | 4 | | | 5 | | | 3 | 6 | -| 7 | | 3 | | 1 | 8 | | | | - -We can codify the rules of Sudoku as a series of constraints in a Theorem: - -#!markdown - -```csharp -public static class SudokuTheorem -{ - public static Theorem Create(Z3Context context) - { - var sudokuTheorem = context.NewTheorem(); - - var cells = typeof(SudokuTable).GetProperties(); - - foreach (var cell in cells) - { - sudokuTheorem = sudokuTheorem.Where(Between1And9(cell)); - } - - sudokuTheorem = sudokuTheorem.Where(DistinctRows(cells)); - sudokuTheorem = sudokuTheorem.Where(DistinctColumns(cells)); - - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell11, t.Cell12, t.Cell13, t.Cell21, t.Cell22, t.Cell23, t.Cell31, t.Cell32, t.Cell33)); - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell14, t.Cell15, t.Cell16, t.Cell24, t.Cell25, t.Cell26, t.Cell34, t.Cell35, t.Cell36)); - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell17, t.Cell18, t.Cell19, t.Cell27, t.Cell28, t.Cell29, t.Cell37, t.Cell38, t.Cell39)); - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell41, t.Cell42, t.Cell43, t.Cell51, t.Cell52, t.Cell53, t.Cell61, t.Cell62, t.Cell63)); - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell44, t.Cell45, t.Cell46, t.Cell54, t.Cell55, t.Cell56, t.Cell64, t.Cell65, t.Cell66)); - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell47, t.Cell48, t.Cell49, t.Cell57, t.Cell58, t.Cell59, t.Cell67, t.Cell68, t.Cell69)); - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell71, t.Cell72, t.Cell73, t.Cell81, t.Cell82, t.Cell83, t.Cell91, t.Cell92, t.Cell93)); - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell74, t.Cell75, t.Cell76, t.Cell84, t.Cell85, t.Cell86, t.Cell94, t.Cell95, t.Cell96)); - sudokuTheorem = sudokuTheorem.Where(t => Z3Methods.Distinct(t.Cell77, t.Cell78, t.Cell79, t.Cell87, t.Cell88, t.Cell89, t.Cell97, t.Cell98, t.Cell99)); - - return sudokuTheorem; - } - - private static Expression> Between1And9(PropertyInfo cellProperty) - { - ParameterExpression tParam = Expression.Parameter(typeof(SudokuTable), "t"); - MemberExpression cell = Expression.Property(tParam, cellProperty); - - ConstantExpression one = Expression.Constant(1, typeof(int)); - ConstantExpression nine = Expression.Constant(9, typeof(int)); - - BinaryExpression cellGreaterThanOrEqual1 = Expression.GreaterThanOrEqual(cell, one); - BinaryExpression cellLessThanOrEqual9 = Expression.LessThanOrEqual(cell, nine); - - var expr = Expression.Lambda>(Expression.And(cellGreaterThanOrEqual1, cellLessThanOrEqual9), new[] { tParam }); - - return expr; - } - - private static Expression> Distinct(PropertyInfo[] cells, string cellPattern) - { - ParameterExpression tParam = Expression.Parameter(typeof(SudokuTable), "t"); - - Expression? distincts = null; - - for (int distinctIndex = 1; distinctIndex <= 9; distinctIndex++) - { - var cellsInDistinct = new List(); - for (int otherIndex = 1; otherIndex <= 9; otherIndex++) - { - var cellName = string.Format(cellPattern, distinctIndex, otherIndex); - - MemberExpression cell = Expression.Property(tParam, cells.Single(_ => _.Name == cellName)); - cellsInDistinct.Add(cell); - } - - NewArrayExpression distinctArray = Expression.NewArrayInit(typeof(int), cellsInDistinct); - MethodCallExpression distinct = Expression.Call(typeof(Z3Methods), "Distinct", new[] { typeof(int) }, distinctArray); - - if (distincts == null) - { - distincts = distinct; - } - else - { - distincts = Expression.And(distincts, distinct); - } - } - - var expr = Expression.Lambda>( - distincts!, - new[] { tParam }); - - return expr; - } - - private static Expression> DistinctColumns(PropertyInfo[] cells) - { - return Distinct(cells, "Cell{1}{0}"); - } - - private static Expression> DistinctRows(PropertyInfo[] cells) - { - return Distinct(cells, "Cell{0}{1}"); - } -} -``` - -#!markdown - -And we can use use the Theorem to express the problem: - -| | | | 2 | 6 | | 7 | | 1 | -|---|---|---|---|---|---|---|---|---| -| 6 | 8 | | | 7 | | | 9 | | -| 1 | 9 | | | | 4 | 5 | | | -| 8 | 2 | | 1 | | | | 4 | | -| | | 4 | 6 | | 2 | 9 | | | -| | 5 | | | | 3 | | 2 | 8 | -| | | 9 | 3 | | | | 7 | 4 | -| | 4 | | | 5 | | | 3 | 6 | -| 7 | | 3 | | 1 | 8 | | | | - -using the following syntax: - -#!csharp - -using (var ctx = new Z3Context()) -{ - var theorem = from t in SudokuTheorem.Create(ctx) - where t.Cell14 == 2 && t.Cell15 == 6 && t.Cell17 == 7 && t.Cell19 == 1 - where t.Cell21 == 6 && t.Cell22 == 8 && t.Cell25 == 7 && t.Cell28 == 9 - where t.Cell31 == 1 && t.Cell32 == 9 && t.Cell36 == 4 && t.Cell37 == 5 - where t.Cell41 == 8 && t.Cell42 == 2 && t.Cell44 == 1 && t.Cell48 == 4 - where t.Cell53 == 4 && t.Cell54 == 6 && t.Cell56 == 2 && t.Cell57 == 9 - where t.Cell62 == 5 && t.Cell66 == 3 && t.Cell68 == 2 && t.Cell69 == 8 - where t.Cell73 == 9 && t.Cell74 == 3 && t.Cell78 == 7 && t.Cell79 == 4 - where t.Cell82 == 4 && t.Cell85 == 5 && t.Cell88 == 3 && t.Cell89 == 6 - where t.Cell91 == 7 && t.Cell93 == 3 && t.Cell95 == 1 && t.Cell96 == 8 - select t; - - var result = theorem.Solve(); - - Console.WriteLine(result); -} - -#!markdown - -## Problem 4 - Missionaries and Cannibals - -#!markdown - -On one bank of a river are three missionaries and three cannibals. - -There is one boat available that can hold up to two people and that they would like to use to cross the river. - -If the cannibals ever outnumber the missionaries on either of the river’s banks, the missionaries will get eaten. - -How can the boat be used to safely carry all the missionaries and cannibals across the river? - -#!markdown - -You can codify the rules as constraints: - -```csharp -var theorem = context.NewTheorem(); - -// Initial state -theorem = theorem.Where(t => t.Missionaries[0] == t.MissionaryAndCannibalCount && t.Cannibals[0] == t.MissionaryAndCannibalCount); - -// Transition model: We filter each step according to legal moves -for (int iclosure = 0; iclosure < maxLength; iclosure++) -{ - var i = iclosure; - //The 2 banks cannot have more people than the initial population - theorem = theorem.Where(t => t.Cannibals[i] >= 0 - && t.Cannibals[i] <= t.MissionaryAndCannibalCount - && t.Missionaries[i] >= 0 - && t.Missionaries[i] <= t.MissionaryAndCannibalCount); - if (i % 2 == 0) - { - // On even steps, the starting bank loses between 1 and SizeBoat people - theorem = theorem.Where(t => t.Cannibals[i + 1] <= t.Cannibals[i] - && t.Missionaries[i + 1] <= t.Missionaries[i] - && t.Cannibals[i + 1] + t.Missionaries[i + 1] - t.Cannibals[i] - t.Missionaries[i] < 0 - && t.Cannibals[i + 1] + t.Missionaries[i + 1] - t.Cannibals[i] - t.Missionaries[i] >= -t.SizeBoat); - - } - else - { - // On odd steps, the starting bank gains between 1 and SizeBoat people - theorem = theorem.Where(t => t.Cannibals[i + 1] >= t.Cannibals[i] - && t.Missionaries[i + 1] >= t.Missionaries[i] - && t.Cannibals[i + 1] + t.Missionaries[i + 1] - t.Cannibals[i] - t.Missionaries[i] > 0 - && t.Cannibals[i + 1] + t.Missionaries[i + 1] - t.Cannibals[i] - t.Missionaries[i] <= t.SizeBoat); - - } - - //Never less missionaries than cannibals on any bank - theorem = theorem.Where(t => (t.Missionaries[i] == 0 || (t.Missionaries[i] >= t.Cannibals[i])) - && (t.Missionaries[i] == t.MissionaryAndCannibalCount || ((t.MissionaryAndCannibalCount - t.Missionaries[i]) >= (t.MissionaryAndCannibalCount - t.Cannibals[i])))); - -} - -// Goal state -// When finished, No more people on the starting bank -theorem = theorem.Where(t => t.Length > 0 - && t.Length < maxLength - && t.Missionaries[t.Length - 1] == 0 - && t.Cannibals[t.Length - 1] == 0 -); -``` - -#!markdown - -Now we have everything we need in order solve the problem. This time, rather than "Solving" the theorem, we use an Optimisation strategy to find the solution with the least number of steps. - -#!csharp - -using (var ctx = new Z3Context()) -{ - var theorem = from t in MissionariesAndCannibals.Create(ctx, 50) - where t.MissionaryAndCannibalCount == 3 - where t.SizeBoat == 2 - orderby t.Length - select t; - - var result = theorem.Solve(); - - Console.WriteLine(result); -} - -#!markdown - -## Problem 5 - 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? - -#!csharp - -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) - select t; - - var result = theorem.Solve(); - - Console.WriteLine(string.Create(CultureInfo.CreateSpecificCulture("en-US"), $"Saudia Arabia: {result.sa} barrels ({(result.sa * 20):C}), Venezuela: {result.vz} barrels ({(result.vz * 15):C})")); -} - -#!markdown - -## Problem 6 - Minimising Shipping Costs - -In this example, you want to minimise 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 minimise 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. - -#!csharp - -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}")); -} diff --git a/solutions/Z3.Linq.Demo/Program.cs b/solutions/Z3.Linq.Demo/Program.cs deleted file mode 100644 index 3ca10ac..0000000 --- a/solutions/Z3.Linq.Demo/Program.cs +++ /dev/null @@ -1,310 +0,0 @@ -namespace Z3.LinqDemo; - -using System; -using System.Diagnostics; -using System.Globalization; - -using Z3.Linq; -using Z3.Linq.Examples; -using Z3.Linq.Examples.RiverCrossing; -using Z3.Linq.Examples.Sudoku; - -public static class Program -{ - private static void Main(string[] args) - { - Console.WriteLine("==== Missionaries & Cannibals using Solve() ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var theorem = from t in MissionariesAndCannibals.Create(ctx, 50) - where t.MissionaryAndCannibalCount == 3 - where t.SizeBoat == 2 - select t; - - var sw = Stopwatch.StartNew(); - MissionariesAndCannibals? result = theorem.Solve(); - sw.Stop(); - - Console.WriteLine(result); - Console.WriteLine($"Time to solution: {sw.Elapsed.TotalMilliseconds} ms"); - Console.WriteLine(); - - Console.WriteLine("==== Missionaries & Cannibals using Optimize() ===="); - Console.WriteLine(); - - sw = Stopwatch.StartNew(); - var minimal = theorem.Optimize(Optimization.Minimize, t => t.Length); - sw.Stop(); - - Console.WriteLine(minimal); - Console.WriteLine($"Time to optimized solution: {sw.Elapsed.TotalMilliseconds} ms"); - Console.WriteLine(); - - Console.WriteLine("==== Missionaries & Cannibals using orderby clause ===="); - Console.WriteLine(); - - sw = Stopwatch.StartNew(); - minimal = (from t in theorem - orderby t.Length - select t).Solve(); - sw.Stop(); - - Console.WriteLine(minimal); - Console.WriteLine($"Time to optimized solution: {sw.Elapsed.TotalMilliseconds} ms"); - } - - Console.WriteLine(); - Console.WriteLine("==== t.x ^ t.y using Anonymous Types ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var theorem = from t in ctx.NewTheorem(new { x = default(bool), y = default(bool) }) - where t.x ^ t.y - select t; - - var result = theorem.Solve(); - - Console.WriteLine(result); - } - - Console.WriteLine(); - Console.WriteLine("==== t.x ^ t.y using ValueTuples ===="); - Console.WriteLine(); - - 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); - ctx.Dispose(); - } - - Console.WriteLine(); - Console.WriteLine("==== t.x ^ t.y using Custom Theorem using Record type ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var theorem = from t in ctx.NewTheorem(new RecordTheorem()) - where t.X ^ t.Y - select t; - - var result = theorem.Solve(); - - Console.WriteLine(result); - } - - Console.WriteLine(); - Console.WriteLine("==== Bart's example from TechEd Europe 2012 ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var theorem = from t in ctx.NewTheorem>() - 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); - } - - Console.WriteLine(); - Console.WriteLine("==== Bart's example from TechEd Europe 2012 using ValueTuples ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var theorem = from t in ctx.NewTheorem<(int x, int y, int z)>() - where t.x - t.y >= 1 - where t.x - t.y <= 3 - where t.x == (2 * t.z) + t.y - select t; - - var result = theorem.Solve(); - - Console.WriteLine(result); - } - - Console.WriteLine(); - Console.WriteLine("==== Example using Symbols ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var theorem = from t in ctx.NewTheorem>() - where t.X1 < t.X2 + 1 - where t.X1 > 2 - where t.X1 != t.X2 - select t; - - var result = theorem.Solve(); - - Console.WriteLine(result); - } - - Console.WriteLine(); - Console.WriteLine("==== SudokuTheorem Example ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var theorem = from t in SudokuTheorem.Create(ctx) - where t.Cell13 == 2 && t.Cell16 == 1 && t.Cell18 == 6 - where t.Cell23 == 7 && t.Cell26 == 4 - where t.Cell31 == 5 && t.Cell37 == 9 - where t.Cell42 == 1 && t.Cell44 == 3 - where t.Cell51 == 8 && t.Cell55 == 5 && t.Cell59 == 4 - where t.Cell66 == 6 && t.Cell68 == 2 - where t.Cell73 == 6 && t.Cell79 == 7 - where t.Cell84 == 8 && t.Cell87 == 3 - where t.Cell92 == 4 && t.Cell94 == 9 && t.Cell97 == 2 - select t; - - var result = theorem.Solve(); - - Console.WriteLine(result); - } - - Console.WriteLine("==== SudokuTheorem Example from https://sandiway.arizona.edu/sudoku/examples.html ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var theorem = from t in SudokuTheorem.Create(ctx) - where t.Cell14 == 2 && t.Cell15 == 6 && t.Cell17 == 7 && t.Cell19 == 1 - where t.Cell21 == 6 && t.Cell22 == 8 && t.Cell25 == 7 && t.Cell28 == 9 - where t.Cell31 == 1 && t.Cell32 == 9 && t.Cell36 == 4 && t.Cell37 == 5 - where t.Cell41 == 8 && t.Cell42 == 2 && t.Cell44 == 1 && t.Cell48 == 4 - where t.Cell53 == 4 && t.Cell54 == 6 && t.Cell56 == 2 && t.Cell57 == 9 - where t.Cell62 == 5 && t.Cell66 == 3 && t.Cell68 == 2 && t.Cell69 == 8 - where t.Cell73 == 9 && t.Cell74 == 3 && t.Cell78 == 7 && t.Cell79 == 4 - where t.Cell82 == 4 && t.Cell85 == 5 && t.Cell88 == 3 && t.Cell89 == 6 - where t.Cell91 == 7 && t.Cell93 == 3 && t.Cell95 == 1 && t.Cell96 == 8 - select t; - - var result = theorem.Solve(); - - Console.WriteLine(result); - } - - Console.WriteLine("==== Oil Purchase Problem. ===="); - Console.WriteLine(); - - using (var ctx = new Z3Context()) - { - var solveable = from t in ctx.NewTheorem<(double vz, double sa)>() - where 0.3 * t.sa + 0.4 * t.vz >= 1900 - where 0.4 * t.sa + 0.2 * t.vz >= 1500 - where 0.2 * t.sa + 0.3 * t.vz >= 500 - where 0 <= t.sa && t.sa <= 9000 - where 0 <= t.vz && t.vz <= 6000 - orderby 20.0 * t.sa + 15.0 * t.vz - select t; - - var result = solveable.Solve(); - - Console.WriteLine(string.Create(CultureInfo.CreateSpecificCulture("en-US"), $"Saudi Arabia: {result.sa} barrels ({(result.sa * 20):C}), Venezuela: {result.vz} barrels ({(result.vz * 15):C})")); - } - - Console.WriteLine(); - Console.WriteLine("==== Warehouse Logistics Problem ===="); - Console.WriteLine(); - - 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}")); - } - - // AllSamplesWithLogging(); - - Console.ReadKey(); - } - - private static void AllSamplesWithLogging() - { - using (var ctx = new Z3Context()) - { - ctx.Log = Console.Out; // see internal logging - - Solve(from t in ctx.NewTheorem(new { x = default(bool) }) - where t.x && !t.x - select t); - - Solve(from t in ctx.NewTheorem(new { x = default(bool), y = default(bool) }) - where t.x ^ t.y - select t); - - Solve(from t in ctx.NewTheorem(new { x = default(int), y = default(int) }) - where t.x < t.y + 1 - where t.x > 2 - select t); - - Solve(from t in ctx.NewTheorem>() - where t.X1 < t.X2 + 1 - where t.X1 > 2 - where t.X1 != t.X2 - select t); - - Solve(from t in ctx.NewTheorem>() - where t.X1 - t.X2 >= 1 - where t.X1 - t.X2 <= 3 - where t.X1 == (2 * t.X3) + t.X5 - where t.X3 == t.X5 - where t.X2 == 6 * t.X4 - select t); - - Solve(from t in ctx.NewTheorem>() - where Z3Methods.Distinct(t.X1, t.X2) - select t); - - Solve(from t in SudokuTheorem.Create(ctx) - where t.Cell13 == 2 && t.Cell16 == 1 && t.Cell18 == 6 - where t.Cell23 == 7 && t.Cell26 == 4 - where t.Cell31 == 5 && t.Cell37 == 9 - where t.Cell42 == 1 && t.Cell44 == 3 - where t.Cell51 == 8 && t.Cell55 == 5 && t.Cell59 == 4 - where t.Cell66 == 6 && t.Cell68 == 2 - where t.Cell73 == 6 && t.Cell79 == 7 - where t.Cell84 == 8 && t.Cell87 == 3 - where t.Cell92 == 4 && t.Cell94 == 9 && t.Cell97 == 2 - select t); - } - } - - private static void Solve(Theorem t) where T : class - { - Console.WriteLine(t); - var res = t.Solve(); - Console.WriteLine(res == null ? "none" : res.ToString()); - Console.WriteLine(); - } -} \ No newline at end of file diff --git a/solutions/Z3.Linq.Demo/Z3.Linq.Demo.csproj b/solutions/Z3.Linq.Demo/Z3.Linq.Demo.csproj deleted file mode 100644 index a778825..0000000 --- a/solutions/Z3.Linq.Demo/Z3.Linq.Demo.csproj +++ /dev/null @@ -1,15 +0,0 @@ - - - - Exe - false - - $(NoWarn);CS1591 - - - - - - - - diff --git a/solutions/Z3.Linq.slnx b/solutions/Z3.Linq.slnx index 7217ab8..834dc44 100644 --- a/solutions/Z3.Linq.slnx +++ b/solutions/Z3.Linq.slnx @@ -10,7 +10,6 @@ -