[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Johannes Waldmann
Subject: Re: [Help-glpk] glpsol (MIP) "-w" output specification, "-y" operation
Date: Fri, 08 May 2009 09:38:53 +0200
User-agent: Thunderbird (X11/20081227)

>> 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,

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
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.

Attachment: signature.asc
Description: OpenPGP digital signature

reply via email to

[Prev in Thread] Current Thread [Next in Thread]