search

endjin / Z3.Linq

LINQ bindings for the Z3 theorem prover from Microsoft Research.
MIT License
29 stars 3 forks source link

Other improvements available #29

Open jsboige opened 10 months ago

jsboige commented 10 months ago

Hi, I just learnt about your project, and I'm very glad you were able to revive it and merge that PR of mine, which had been left hanging. I just wish I had known about your project earlier. Now I'm wondering, my latest developments were made to that other branch. Did you see it when you merged? It's a bit messy as I was adding to it as part of a teaching course and there is this "meal planner" example with loads of Data that needed some more work, but I believe if you do a comparison on the main core files, there might be significant contributions to add here. Also, by the time I did my PR, the Ricardo Niepel had started working on this other project that is also dead and would have plenty code to bring. We should probably ask him about it.

Well this is to say, now that I know about your project, I'll try and find some time to become a regular contributor.

Cheers

HowardvanRooijen commented 10 months ago

Hello! I'm so glad you found this project and are happy that we pulled in some of your contributions - it seemed a waste to leave all these disparate forks, so we tried out best to pull in all the changes we understood into the codebase.

I think I did see you "newest" branch. I think at the time I didn't really understand the context of what you were trying to do, what the code changes supported or if the data you had in that branch was open or proprietary and then we ran out of time for out initial modernisation efforts.

Obviously, we'd love any further contributions. I do think that the combination of Polyglot Notebooks and Z3.Linq is really powerful - especially if you're teaching.

I'm personally very interested in what you're doing with Semantic Kernel too - again there might be some synergies there too as we're exploring that domain (and OpenAI etc) too.

/cc @colombod

jsboige commented 10 months ago

Hi, thanks for your message. I'll take some time to review what was merged and not in the following weeks when I'm done with my current SK's contributions, and I'll make you a couple PRs, with improvements into the core, and with that extra meal planner example, which did contain only open-data, but needs some more clean-up. And yes, there might be interesting synergies between semantic-kernel and what this library does. I'll look into that too.

HowardvanRooijen commented 10 months ago

I'm very interesting in this library to see how:

a) we can integrate it into https://github.com/dotnet/reactive and https://github.com/reaqtive/reaqtor so that we can run solvers based on reactive inputs b) how we can integrate solvers into more generalised knowledge graph / AI

I would also love to resurrect Solver Foundation, as this offers a much more extensible approach to building solvers /cc @luisquintanilla

jsboige commented 10 months ago

@HowardvanRooijen I'm definitely interested into your work with reactive extensions too.

Just to give you a bit of context with my past contributions to this lib.

All of that was part of an AI course that I teach to several engineering schools in France, as one of my regular assessments is implementing Sudoku solvers in a number of different ways. Those guys for instance have pretty much rinced the topic leveraging raw Z3's API, and those ones were supposed to accommodate the same ideas into LinqToZ3 (adding substitution API and bitvector support), but they reverted to the raw API instead (unfortunately they deleted their repo with my PR's instruction with actual line numbers, but I guess I could figure that again).

I have plenty of such repos where group of students have implemented and pushed various Sudoku solvers under my supervision using libraries for Search, Symbolic, Probabilistic and even Neural Nets APIs. I also demonstrated a Solver foundation's implementation at some point, although the lack of .Net core support didn't help, and I agree it's a shame that lib died. I would provide a central Benchmarking console App, which gave an idea on how z3 and linq2z3 perform as compared to other libs. Well let's say there's room for improvements. OR-Tools, Chocosolver+IKVM etc. tend to have a more efficient SAT core than Z3 at least on that problem and a few others, and linq2Z3 is an order of magnitude behind, though I suppose the difficulty range here is specifically in the wrong spot. Then I suppose Z3 being an SMT isn't meant to rival powerful SATs and CSP solvers, and it's more about the theories it supports.

HowardvanRooijen commented 10 months ago

If you're teaching, I'm sure @colombod would be interested as I know he engages with a number of universities. He and @jonsequitur work on https://github.com/dotnet/interactive/ (AKA Try.NET & Polyglot Notebooks).

I would very much like to open source & modernise Solver Foundation and have talked to @luisquintanilla that a number of real world business problems, get described to us a "Travelling Sales Person Type Problems" because that's the only analogy the customer can think of to describe what is essentially an Operational Research problem, and that many initial use cases customer gets excited about AI (and LLMs) are really Operational Research ones, like supply chain, logistics or price optimisation problems that Solvers are a better solution for. Z3 / Solver Foundation was 15 years too early, but now with the current AI boom, it's the perfect time to re-introduce them and highlight their relevance.

jsboige commented 10 months ago

If you're teaching, I'm sure @colombod would be interested as I know he engages with a number of universities. He and @jonsequitur work on https://github.com/dotnet/interactive/ (AKA Try.NET & Polyglot Notebooks).

I have tons of AI c# teaching material that need turned into notebooks (including those 20+ Sudoku solvers that could make for a great series). Hopefully I'll manage to find some time for that this year.

I would very much like to open source & modernise Solver Foundation and have talked to @luisquintanilla that a number of real world business problems, get described to us a "Travelling Sales Person Type Problems" because that's the only analogy the customer can think of to describe what is essentially an Operational Research problem, and that many initial use cases customer gets excited about AI (and LLMs) are really Operational Research ones, like supply chain, logistics or price optimisation problems that Solvers are a better solution for. Z3 / Solver Foundation was 15 years too early, but now with the current AI boom, it's the perfect time to re-introduce them and highlight their relevance.

Well don't get me started on the topic. The .Net AI landscape is a graveyard. Infer has been on life support for a couple years, even ML.Net and Spark.Net seem to be struggling, which is really a shame considering Accord.Net and CNTK are dead for good and the SciSharp team has been struggling on so many fronts. Well I could go on and on with many other individual tragedies from the past decade. IronPython and IKVM could bring some serious relief, but they're also struggling with outdated distributions and tooling, Python.Net works well but bridging is not nearly the same.

This to say I'm very grateful you guys didn't let this great project go to waste. Reviving Solver foundation would definitely be great too.

HowardvanRooijen commented 10 months ago

Infer.net now lives under the umbrella of ML.NET as Microsoft.ML.Probabilistic (and a MIT License). A bit like Rx I thought it was a very mature library that just needed light touch maintenance...

There's a huge amount of value in ML.NET the only problem is that OpenAI (and LLMs in general) is drowning out more classic forms of ML.

jsboige commented 10 months ago

Infer.net now lives under the umbrella of ML.NET as Microsoft.ML.Probabilistic

I know, but it's been stalled pretty much precisely since the decision was made. I believe that lib has immense merits and @tminka has poured his heart into it, but the migration of many examples was half baked at that time (tutorial browser wasn't core compatible), and well not many people dare get into the world of conjugate prior distributions, which arguably is quite intimidating (mbml book was supposed to change that, but it fell short with publishing mistakes I believe). In the mean time Pyro, Tensorflow probability, Pymc and others have kept moving, just like with other AI branches...

jsboige commented 10 months ago

it's been stalled pretty much precisely since the decision was made.

Actually, there is a bit of a pattern here. I know this isn't the case with your project, but it's as if putting projects under the umbrella of .Net foundation would bring some kind of magic protection. Well it's been pretty much the opposite many times.

HowardvanRooijen commented 10 months ago

I think people completely misunderstand the purpose of the .NET Foundation. It's not suddenly going to magic up a budget and engineering resources to maintain a project, but it does offer a good legal framework and guardianship longevity meaning that access to a project can outlive any single maintainer. This process is what allowed us to take over maintenance of Rx .NET. Open Source is all about people contributing effort. If no-one contributes (even for purely selfish reasons - i.e. this component is part of my software supply chain), then entropy kicks in and things don't just stand still, "bit-rot" sets in and the technical debt increases.

jsboige commented 10 months ago

Well we both talked of magic, I guess we're on the same line. I still resent Ms for not bringing the relief they could have in time. Again, an IronPython that let you "Nugget Pip packages" in Bytecode with near to identical performances and a cristal clear public members' surface was and still is a couple man's years work away. It would pay for itself a thousand times...