Hi Nicolas:

Actually the old and new above is reversed.
And yes, each Command now embeds the formula it is trying to satisfy,
so to solve a command you just give that command to the execute_command() method

(This API change is needed because of the upcoming "greedy solving"
feature where a Command can now embed a series of different formula
that should be satisfied at different stages...)

>
> Are there any other changes to the API that I should be concerned about?
>

I think that was it.  But as a clarification, I should remind users
that the formula you embed with a Command must be "everything" you want to be true.
So in general, if we use the Alloy textual language as an analogy:

fact A { ... }
fact B { ... }
pred C { ... }
run C

Then the formula you give to a Command object must be "A and B and C"
That is, at the API level, we don't know what formula is a fact and what is not,
so you need to add the ones you care about into the Command object.

Thanks for the clarifications Felix!

This incremental feature sounds nice; I wonder if it can help me do the following:

fact A { ... }
fact B { ... }

pred C1 { ... }
pred C2 { ... }
pred C3 { ... }

// try solving C1, C2, C3 sequentially until one returns UNSAT.

run A & B & C1
if C1 is satisfied, then run A & B & C2
if C2 is satisfied, then run A & B & C3

If it does, how about the following:

fact A { ... }
fact B { ... }

pred C1 { ... }
assert C1Sat { ... }

pred C2 { ... }
assert C2Sat { ... }

pred C3 { ... }

// try solving C1, C2, C3 sequentially with additional constraints at each step until we get UNSAT

run A & B & C1
if C1 is satisfied, then run A & B & C1Sat & C2
if C2 is satisfied, then run A & B & C1Sat & C2Sat & C3

Nicolas Rouquette
Flight Software Engineering & Architecture Group
Jet Propulsion Laboratory, Caltech, Pasadena, CA, USA

Hi Nicolas:

First of all, I need to rephrase my previous answer.
I should have said the new feature is "greedy solving" rather than
"incremental solving" (which has a very well known meaning in SAT Solver literature)

(I just edited my answer above to say "greedy solving")

Incremental Solving
====================

To illustrate "incremental solving" (which we want to implement eventually
but we don't have the number of students needed to do this right now):

solve A
If satisfiable, solve A && B
If still satisfiable, solve A && B && C

End result:

if (A && B && C) is satisfiable,
we are guaranteed to find it eventually.

If (A && B && C) is unsatisfiable,
we are guaranteed to confirm it eventually.

Furthermore, if (A && B) is satisfiable, but (A && B && C) is not,
we would also discover that and we can show you the instance that satisfies (A && B)
while also telling you that (A && B && C) is impossible.

(When done properly, this would be extremely efficient:
we would keep a SAT solver instance in memory,
and progressively feed it more clauses, so the cost would be
similar to doing one solve rather than doing 3 separate solves)

Greedy Solving
==============

To illustrate "greedy solving" (which should be in Alloy 4.2):

solve A
If satisfiable, then solve B by extending the existing instance with possibly larger scope
If still satisfiable, then solve C by extending the existing instance with possibly larger scope

End result:

If we get an instance at the end, then it is guaranteed to satisfy (A && B && C).

If we don't get an instance at the end, then it doesn't tell us anything.
It may be that (A && B && C) is truly unsatisfiable.
On the other hand, perhaps (solve A) gave us an unlucky instance
in which it is impossible to further extend it to satisfy (A && B && C).

(Of course my tool will memorize the last successful solve;
if (solve A) succeeds but (extend then solve B) fails,
then we will show you the instance that satisfied A
while telling you that this greedy approach was unable to find an instance satisfying (A && B))

> Example 1
> =========
> fact A { ... }
> fact B { ... }
> pred C1 { ... }
> pred C2 { ... }
> pred C3 { ... }
> // try solving C1, C2, C3 sequentially until one returns UNSAT.
> run A & B & C1
> if C1 is satisfied, then run A & B & C2
> if C2 is satisfied, then run A & B & C3

In this first example here, unfortunately it is neither Incremental Solving nor Greedy Solving.
(I assume your C1 and C2 and C3 are potentially contradictory?)

That is, you literally, as you said, want to try running (A & B & C1)
then (A & B & C2) then (A & B & C3) individually, and want to stop the solver
when you see the first UNSAT, but the instances you get from the first solve
is not used as a limiting constraint in the second solve?

If my assumption about your question is correct,
then the new feature won't offer any advantage here.
You would have to run the 3 solves individually just like right now.

> Example 2
> =========
> fact A { ... }
> fact B { ... }
> pred C1 { ... }
> assert C1Sat { ... }
> pred C2 { ... }
> assert C2Sat { ... }
> pred C3 { ... }
> // try solving C1, C2, C3 sequentially with additional constraints at each step until we get UNSAT
> run A & B & C1
> if C1 is satisfied, then run A & B & C1Sat & C2
> if C2 is satisfied, then run A & B & C1Sat & C2Sat & C3

What is the relationship between C1 and C1Sat?  Are they the same?

That is, ignoring the syntax difference of fact/pred/assert for the moment,
and let's just talk abstractly about a list of unrelated formulas A B C1 C2 C3.
Is your question about doing this:

run A & B & C1
If satisfiable, run A & B & C1 & C2
If still satisfiable, run A & B & C1 & C2 & C3

If that's your question, then that is the classic "incremental solving" situation.

When Alloy adds Incremental Solving (perhaps next year?) it will solve this perfectly.

When Alloy adds Greedy Solving (probably next month or so) it will solve this sometimes.
That is, if Alloy greedy solver gives you an answer at the end for the final step,
that means indeed we found a solution that satisfied A B C1 C2 C3.
But if Alloy greedy solver does not find a solution at the very end for the final step,
then it gives us no information.

Sincerely,
Felix Chang
Alloy4 Developer