> I will write a solver for formulas-over-model using QeCode. I think
> this will solve our problems, although I'm sure it will not be a
> "SAT-killer".
>
> The boolean algebra is definable over MSO variables, but it would be
> more solver-efficient if introduced "natively".
That would be very nice, especially as QeCode could be extended
to handle real numbers in the future. But there are two questions
you have to ask yourself now: (1) Is this realy doable in short time?
If not, it will probably be better to do it together with other people
interested in solvers, as this can be hard work. (2) Will it at some
point be at least comparable with SAT solvers? If not, we should
rethink the whole design with other people, we cannot allow truly
suboptimal solutions by design.
> I propose to add set inclusion and set equality to the language
> (oh well, the latter overloading the = symbol.) Throw your ideas
> for the set inclusion syntax (my proposal is to overload "in",
> "x in Y" vs "Y in Z").
>
> I will also extend the FO part with a poly-ary "Distinct" primitive.
> E.g. Distinct {x,y,z} <-> x =/= y and y =/= z and x =/= z, but only
> allowed for first-order variables.
Yes, at some point we will have to add such syntactic
shorthands anyway, so do it whenever you feel like it :).
I do not care so much about syntax, but X c Y, X <= Y
and X subset Y could be considered as well, as well as
other, e.g. X union Y or X intersection Y. The naming
scheme should be consistent, i.e. either full names for
everything (I think I prefer that) or symbols of some kind
for everything. Also, 'in' can be problematic if one day we
add some hierarchy and elements start having elements (soä
X in Y might then mean level-1 set in level-2 set as element).
Lukasz Kaiser
|
