Re: [Help-glpk] glpsol (MIP) "-w" output specification, "-y" operation

[Johannes Waldmann]

>> Z = SUM Bz[j, k]*max(j, k)
>>    j,k

yes, that's basically a unary encoding of numbers as bit strings.
If I'm taking that route, I can go all the way and use *only* booleans.
Then it's a SAT problem, and there are very good solvers for these,
see http://www.satcompetition.org/

With SAT I get "for free" arbitrary boolean combinations
of constraints (with LP/MIP, it's just conjunction).
And I can also use binary encoding (instead of unary) -
less unknowns but more constraints.

I guess for constraints with min/max/plus,
the right framework is SMT/QF_LRA
http://combination.cs.uiowa.edu/smtlib/logics/QF_LRA.smt
and then using a DPLL(T) solver.

I'll give MIP one more try, though,
reducing the "big M" as far as possible.

Best regards, Johannes.


PS: I was asking about the differences between gmpl and (e.g.) zimpl.
What is the common subset? Ideally, I'd be able to just switch solvers,
but have identical input and output formatting.
The competitions mentioned above (SAT, SMT) do enforce this, in their area.

signature.asc
Description: OpenPGP digital signature