Constraint Solver
77 views
Skip to first unread message
Allan Gardner
Jul 24, 2014, 12:45:34 AM7/24/14
to diagrams-discuss
The first half of my project was refactoring diagrams-lib to not
hard-code Double; this is done except for renaming R2ISh to R2 and
fixing the backends. See the generalize-double branch and issue #50 in
diagrams-lib.
The second half of my project is finding a constraint solver and
connecting diagrams to it in a useful way. I've read through all of
Hackage and besides finding some interesting libraries (there are 4
color packages: colors, colour, prizm, and wright; and 'tau' and
'splines' packages that diagrams doesn't use), I created a list of
possible constraint solvers.
The first category are SMT solvers; although they're probably not a
great fit for the project, there does seem to be somewhat
well-maintained bindings for Yices, Z3, and CVC4. The Yices page
claims it can solve sets of linear constraints.
But if all I have are sets of linear constraints, and I want to solve
them with an SMT solver, then I could just use linearEqSolver, which
wraps the SMT solvers and gives me a single function
solveRationalLinearEqs. Or I could use the linear programming thing of
toysolver, or implement a more complex linear solver like the
Cassowary algorithm (used in Apple's Cocoa UI kit for laying out
buttons and other elements).
If we go to nonlinear stuff, then there are still a few options left.
There are implements of nonlinear optimization, namely
hmatrix-quadprogpp, lagrangian, levmar and nonlinear-optimization,
almost all of which can optimize in the presence of linear constraints
as well. It's a simple nearest-extrema search though so I'm not
certain how well it can lay out diagrams.
The final library I've found is GECODE, "generic constraint
development environment", which allows specifying all of the above:
arbitrary linear constraints, arbitrary nonlinear constraints, and
arbitrary nonlinear optimization criteria. I haven't really delved
into the source code too deeply, so maybe the API promises more than
it can deliver. There's also the issue of the bindings
(monadiccp-gedcode), which are to version 3.1.0 (released in 2009)
instead of to the latest version (4.2.1, released last year). I've
sent an email to the maintainer on Monday but no response yet.
Anyways, dear diagrams-discuss, which solver should I use? Did I miss
any in my review of Hackage, or are there some non-yet-uploaded
solvers floating around on Github?
Finally, there is the question of "usefulness"; I asked my mentor for
a simple example of when you would need to use constraint solving in
diagrams, and he was unable to think of one off the top of his head. I
searched the web and found
http://www.skybluetrades.net/blog/posts/2011/11/14/constraints-intro.html,
whose reasoning was roughly "I used AutoDesk’s Mechanical Desktop for
a work project and it was really cool and a Haskell clone would be
even cooler", but at least he had an example. Cassowary has spawned a
whole literature on UI layout algorithms, which I've been slowly
working through; they're OK but very focused on interactive layout. In
terms of diagrams this is only relevant for animations, which do seem
to be under-developed so maybe I should work on that too?
I get to discuss all of this with bergey tomorrow at 17:00 UTC (i.e.,
in 12 hours), so feel free to join us in #diagrams then.
-- Allan Gardner
hard-code Double; this is done except for renaming R2ISh to R2 and
fixing the backends. See the generalize-double branch and issue #50 in
diagrams-lib.
The second half of my project is finding a constraint solver and
connecting diagrams to it in a useful way. I've read through all of
Hackage and besides finding some interesting libraries (there are 4
color packages: colors, colour, prizm, and wright; and 'tau' and
'splines' packages that diagrams doesn't use), I created a list of
possible constraint solvers.
The first category are SMT solvers; although they're probably not a
great fit for the project, there does seem to be somewhat
well-maintained bindings for Yices, Z3, and CVC4. The Yices page
claims it can solve sets of linear constraints.
But if all I have are sets of linear constraints, and I want to solve
them with an SMT solver, then I could just use linearEqSolver, which
wraps the SMT solvers and gives me a single function
solveRationalLinearEqs. Or I could use the linear programming thing of
toysolver, or implement a more complex linear solver like the
Cassowary algorithm (used in Apple's Cocoa UI kit for laying out
buttons and other elements).
If we go to nonlinear stuff, then there are still a few options left.
There are implements of nonlinear optimization, namely
hmatrix-quadprogpp, lagrangian, levmar and nonlinear-optimization,
almost all of which can optimize in the presence of linear constraints
as well. It's a simple nearest-extrema search though so I'm not
certain how well it can lay out diagrams.
The final library I've found is GECODE, "generic constraint
development environment", which allows specifying all of the above:
arbitrary linear constraints, arbitrary nonlinear constraints, and
arbitrary nonlinear optimization criteria. I haven't really delved
into the source code too deeply, so maybe the API promises more than
it can deliver. There's also the issue of the bindings
(monadiccp-gedcode), which are to version 3.1.0 (released in 2009)
instead of to the latest version (4.2.1, released last year). I've
sent an email to the maintainer on Monday but no response yet.
Anyways, dear diagrams-discuss, which solver should I use? Did I miss
any in my review of Hackage, or are there some non-yet-uploaded
solvers floating around on Github?
Finally, there is the question of "usefulness"; I asked my mentor for
a simple example of when you would need to use constraint solving in
diagrams, and he was unable to think of one off the top of his head. I
searched the web and found
http://www.skybluetrades.net/blog/posts/2011/11/14/constraints-intro.html,
whose reasoning was roughly "I used AutoDesk’s Mechanical Desktop for
a work project and it was really cool and a Haskell clone would be
even cooler", but at least he had an example. Cassowary has spawned a
whole literature on UI layout algorithms, which I've been slowly
working through; they're OK but very focused on interactive layout. In
terms of diagrams this is only relevant for animations, which do seem
to be under-developed so maybe I should work on that too?
I get to discuss all of this with bergey tomorrow at 17:00 UTC (i.e.,
in 12 hours), so feel free to join us in #diagrams then.
-- Allan Gardner
Chris Mears
Jul 24, 2014, 3:05:57 AM7/24/14
to diagrams...@googlegroups.com
On Thu, 24 Jul 2014 06:45:33 +0200
Allan Gardner <allane...@gmail.com> wrote:
> The first category are SMT solvers; although they're probably not a
> great fit for the project, there does seem to be somewhat
> well-maintained bindings for Yices, Z3, and CVC4. The Yices page
> claims it can solve sets of linear constraints.
I think an SMT solver could be a good fit for the project, although I
Allan Gardner <allane...@gmail.com> wrote:
> The first category are SMT solvers; although they're probably not a
> great fit for the project, there does seem to be somewhat
> well-maintained bindings for Yices, Z3, and CVC4. The Yices page
> claims it can solve sets of linear constraints.
don't know what exactly sort of constraints you're going to solve. As
long as the theory (the T part of the SMT) supports linear constraints,
you should be OK.
An advantage of an SMT solver over a plain linear solver is that it
should do a better job of simple disjunctions, such as those that arise
from non-overlap constraints. For example, you might say that one
subdiagram must be either to the left or to the right of another
subdiagram.
> The final library I've found is GECODE, "generic constraint
> development environment", which allows specifying all of the above:
> arbitrary linear constraints, arbitrary nonlinear constraints, and
> arbitrary nonlinear optimization criteria. I haven't really delved
> into the source code too deeply, so maybe the API promises more than
> it can deliver. There's also the issue of the bindings
> (monadiccp-gedcode), which are to version 3.1.0 (released in 2009)
> instead of to the latest version (4.2.1, released last year). I've
> sent an email to the maintainer on Monday but no response yet.
mentioned in that it works with arbitrary constraints, primarily over
finite domain variables. This means it will be weaker if you have
mainly linear constraints over continuous variables, but might be
better if you have more complex constraints that can't be expressed
easily or solved efficiently with the other kinds of solver.
> Anyways, dear diagrams-discuss, which solver should I use? Did I miss
> any in my review of Hackage, or are there some non-yet-uploaded
> solvers floating around on Github?
(http://www.minizinc.org/), which is a language for modelling
constraint problems. You could use MiniZinc to express the problem,
then use some solver to find the solution. One advantage of this
approach is that you can use different kinds of solver, such as Gecode
or a MIP solver like SCIP (http://scip.zib.de/), without having to
translate your model.
Yet another approach is to write your own solver, which is not
necessarily as scary as it sounds. A colleague of mine has written
an interactive graph layout library in Javascript, and the core solving
component turns out to be not very big even though it supports
non-overlap and alignment constraints and is fast enough for
interactive use. (See
http://marvl.infotech.monash.edu/webcola/examples/smallnonoverlappinggraph.html
and http://marvl.infotech.monash.edu/webcola/examples/alignment.html
for examples.) But this might be a bit much for your project.
Unfortunately I can't make your IRC meeting with bergey, but I'll leave
my client idling in there and read the discussion when I can.
Allan Gardner
Jul 28, 2014, 4:38:33 PM7/28/14
to diagrams...@googlegroups.com
On Thu, Jul 24, 2014 at 1:05 AM, Chris Mears <ch...@cmears.id.au> wrote:
> On Thu, 24 Jul 2014 06:45:33 +0200
> Allan Gardner <allane...@gmail.com> wrote:
>
>> The first category are SMT solvers; although they're probably not a
>> great fit for the project, there does seem to be somewhat
>> well-maintained bindings for Yices, Z3, and CVC4. The Yices page
>> claims it can solve sets of linear constraints.
>
> I think an SMT solver could be a good fit for the project, although I
> don't know what exactly sort of constraints you're going to solve. As
> long as the theory (the T part of the SMT) supports linear constraints,
> you should be OK.
>
> An advantage of an SMT solver over a plain linear solver is that it
> should do a better job of simple disjunctions, such as those that arise
> from non-overlap constraints. For example, you might say that one
> subdiagram must be either to the left or to the right of another
> subdiagram.
>
So for those who do not follow IRC, I have decided to use the sbv
> On Thu, 24 Jul 2014 06:45:33 +0200
> Allan Gardner <allane...@gmail.com> wrote:
>
>> The first category are SMT solvers; although they're probably not a
>> great fit for the project, there does seem to be somewhat
>> well-maintained bindings for Yices, Z3, and CVC4. The Yices page
>> claims it can solve sets of linear constraints.
>
> I think an SMT solver could be a good fit for the project, although I
> don't know what exactly sort of constraints you're going to solve. As
> long as the theory (the T part of the SMT) supports linear constraints,
> you should be OK.
>
> An advantage of an SMT solver over a plain linear solver is that it
> should do a better job of simple disjunctions, such as those that arise
> from non-overlap constraints. For example, you might say that one
> subdiagram must be either to the left or to the right of another
> subdiagram.
>
library (http://hackage.haskell.org/package/sbv).
-- Allan Gardner
Reply all
Reply to author
Forward
0 new messages