CP contraints and boolean logic

Jan 15, 2015 at 6:59 AM
Hello,

I dove into CP recently and got my feet wet using Google OR-tools. Not a bad library, but I would like to do some boolean logic with my constraints.

I am generally familiar with CP. I also familiar with Microsoft Solver Foundation, but it seems that this library has been abandoned in who knows what condition.

How does Z3 compare, contrast, stand on is own where CP is concerned?

I am mainly interested in a 'managed', C# .NET, but who knows...

Thank you...
Jan 15, 2015 at 6:26 PM
Maybe I am missing something, but examples that used to call out AssertCnstr or CheckAndModel are broken, these functions do not exist in version 4.x? Do I need another assembly?

Where might I find some halfway decent docs for .NET, C#, etc?

Thank you...
Coordinator
Jan 15, 2015 at 8:06 PM
The .NET API was replaced with a completely new API when we transitioned from 3.x to 4.x, so yes, you need to use the new ones. The API documentation is available here: .NET API docs and Z3 comes with an example program, but that is not included in the binary distributions. It does come with the sources or directly from the repository, here: .NET Example
Jan 15, 2015 at 8:35 PM
Thank you for the response.

I am reading a couple of the examples. Perhaps I don't understand, why does Prove throw an exception on SATISFIABLE, and Disprove on UNSATISFIABLE? I would think that should be the other way round?
Coordinator
Jan 15, 2015 at 8:40 PM
No, those are the right way round. Note that both functions negate the constraint at
s.Assert(ctx.MkNot(f));
If the negation of f is satisfiable, that means that the constraints can be violated, i.e., the "test" failed and we throw an exception. Conversely, in Disprove we are actively trying to find a way to violate the constraint, but if there is absolutely no way to do so (i.e., the negation of f is unsatisfiable), then we throw an exception.
Jan 15, 2015 at 9:26 PM
Is there some help in the form of glossary, definitions of terms.

For example, I am familiar with "model", "variable", and "constraints", in CP and CSP terms. I don't know quite what the analogs are, apart from the vocabulary seems much more detailed.

This is okay, as long as I can determine "here's what a goal is", "this is what a tactic is", etc.

Estimated, probably a couple of days working with the framework before it becomes familiar.

Thanks...
Jan 15, 2015 at 9:34 PM
Additionally, studying some of the example code, "BasicTests", and the lines of code within, apart from showing syntactically what's going on, doesn't really tell me what sort of problem is being solved. The lines of code are interesting, but it doesn't really add anything to my comprehension of the API.
Coordinator
Jan 16, 2015 at 12:26 PM
The terminology that we use is largely based on the SMT language (and vice versa). The only part that is really confusing for new users is that "variables" are only explicitly quantified variables. Non-quantified variables are called "constants", because they are "constant functions". For a tutorial please see the Z3 Guide and our other tutorials. The terminology used in them is the same that is used in all our APIs, so we don't need separate tutorials for each of them. Note that goals/tactics/etc are actually Z3-specific extensions, but there is a separate tutorial on those topics: strategies tutorial.

There is also David Cok's excellent SMT2 Tutorial that might help.