Guan in the combinatorics landscape

[d-vyd]

I've been reading about first order logic, SAT, and SMT concepts and tools and it occurred to me that Microsoft's Z3 has already been applied to software, hardware, and even manufacturing plant configurations. My understanding is that Z3 is highly optimized for combinatorics. Fabric-Healer could have been built on Z3, right? Yet, you kind folks decided to create Guan with Prolog syntax and make it available to the world. What is Guan's niche compared to Z3, either generally or specific to configuration-as-logic?

[GitTorre]

For FH, a theorem prover like Z3 is way too complex for the problem domain. It would be like flying an A380 from Seattle to Portland when all you really need is an A320 or a Boeing 737 or even a propeller aircraft given the problem domain (distance from a to b, passenger volume, aircraft design (A380 is for taking lots of people very far), etc.)

FH represents a very narrow problem domain:

Given a set of facts about the health state of a Service Fabric entity, like a service, enable human-friendly, logically precise, "runnable specification" - or user configuration - that describes a workflow that unambiguously leads to some mitigation goal state.

This problem domain is perfect for logic programming (in fact, it is the definition of logic programming: programming by description, runnable configuration, logical expression...) and Guan is easy to use. In fact, Guan was worked on (as a stand-alone library shipped as a nupkg) specifically so that FH could adopt it (Guan was used initially as a logic programming facility in a larger project (internal) with a much grander problem domain than that of FH..).

I can't speak to your other questions as they are outside my area of expertise.

[d-vyd]

That makes sense. To me, FH looked complicated but I do understand what you mean about Z3 versus a traditional logic programming language. The latter is far easier for ordinary humans to follow.