News for hackers. Stuff that matters.

A comment on A CP Solution for XKCD NP Complete Restaurant Order.

Re:A CP Solution for XKCD NP Complete Restaurant Order by krenoten on Tuesday May 28, 2013 @10:59AM (#5780403)
Is the Z3 theorem prover an example of a CP tool? For those interested, Z3 is one of the world's fastest theorem provers and has been open sourced by Microsoft. Theorem provers have many interesting applications, but one of my favorites is using them to represent a program's state and reasoning about the exploitability of bugs. It has bindings to C, C++, .NET and Python. Check it out if it interests you: http://z3.codeplex.com/ or try it online at http://rise4fun.com/z3py
[ Parent | on HN ]
Re:A CP Solution for XKCD NP Complete Restaurant Order by nitrogen on Tuesday May 28, 2013 @12:43PM (#5781035)
Before you download Z3 and dive in, be aware that Z3 is not Open Source. It's licensed under a non-commercial license[0], which is not compatible with the Open Source definition[1]. Muddying the term Open Source will diminish its descriptive usefulness.

[0] http://z3.codeplex.com/SourceControl/latest#LICENSE.txt

[1] http://opensource.org/osd#fields-of-endeavor

[ Parent | on HN ]
Re:A CP Solution for XKCD NP Complete Restaurant Order by colanderman on Tuesday May 28, 2013 @11:05AM (#5780437)
Z3 is based on SMT (satisfiability-modulo-theories), not constraint programming. You can probably do some constraint programming in it, but that's not what it's designed for.
[ Parent | on HN ]