Z3
Z3 is a theorem prover from Microsoft Research.
Visit Z3 ↗- Type
- Audience
Related resources
- HuubSolverHuub is a Lazy Clause Generation (LCG) solver with a focus on modularity and maintainability in addition to speed. LCG solvers are a class of solvers that can be used to solve decision and optimization problems. They are characterized by their ability to dynamically add new Boolean variables and clauses to a Boolean Satisfiability (SAT) solver during the search process
- GecodeSolverGecode is an open source C++ toolkit for developing constraint-based systems and applications. Gecode provides a constraint solver with state-of-the-art performance while being modular and extensible.
- CP ConferenceConferenceInternational conference about Constraint Programming
- CPAIORConferenceInternational conference about the integration of Constraint Programming, Artificial Intelligence and Operations Research
- Meinolf SellmanContent creatorCreator of Optimization Solvers, CEO at InsideOpt.
- MiniZincModeling languageMiniZinc is a high-level constraint modelling language that allows you to easily express and solve discrete optimisation problems.