Constraint programming allows difficult combinatorial problems to be modelled declaratively and solved automatically. Advances in solver technologies over recent years have allowed the successful use of constraint programming in many application areas. However, when a particular solver's search for a solution takes too long, the complexity of the constraint program execution hinders the programmer's ability to profile that search and understand how it relates to their model. Therefore, effective tools to support such profiling and allow users of constraint programming technologies to refine their model or experiment with different search parameters are essential. This paper details the first user-centred design process for visual profiling tools in this domain. We report on: our insights and opportunities identified through an on-line questionnaire and a creativity workshop with domain experts carried out to elicit requirements for analytical and visual profiling techniques; our designs and functional prototypes realising such techniques; and case studies demonstrating how these techniques shed light on the behaviour of the solvers in practice.

Drawings of highly connected (dense) graphs can be very difficult to read. Power Graph Analysis offers an alternate way to draw a graph in which sets of nodes with common neighbours are shown grouped into modules. An edge connected to the module then implies a connection to each member of the module. Thus, the entire graph may be represented with much less clutter and without loss of detail. A recent experimental study has shown that such lossless compression of dense graphs makes it easier to follow paths. However, computing optimal power graphs is difficult. In this paper, we show that computing the optimal power-graph with only one module is NP-hard and therefore likely NP-hard in the general case. We give an ILP model for power graph computation and discuss why ILP and CP techniques are poorly suited to the problem. Instead, we are able to find optimal solutions much more quickly using a custom search method. We also show how to restrict this type of search to allow only limited back-tracking to provide a heuristic that has better speed and better results than previously known heuristics.

We explore the effectiveness of visualizing dense directed graphs by replacing individual edges with edges connected to 'modules'-or groups of nodes-such that the new edges imply aggregate connectivity. We only consider techniques that offer a lossless compression: that is, where the entire graph can still be read from the compressed version. The techniques considered are: a simple grouping of nodes with identical neighbor sets; Modular Decomposition which permits internal structure in modules and allows them to be nested; and Power Graph Analysis which further allows edges to cross module boundaries. These techniques all have the same goal--to compress the set of edges that need to be rendered to fully convey connectivity--but each successive relaxation of the module definition permits fewer edges to be drawn in the rendered graph. Each successive technique also, we hypothesize, requires a higher degree of mental effort to interpret. We test this hypothetical trade-off with two studies involving human participants. For Power Graph Analysis we propose a novel optimal technique based on constraint programming. This enables us to explore the parameter space for the technique more precisely than could be achieved with a heuristic. Although applicable to many domains, we are motivated by--and discuss in particular--the application to software dependency analysis.

For constraint programming, many well performing dynamic symmetry breaking techniques have been devised. For propositional satisfiability solving, dynamic symmetry breaking is still either slower or less general than static symmetry breaking. This paper presents Symmetry Propagation, which is an improvement to Lightweight Dynamic Symmetry Breaking, a dynamic symmetry breaking approach from CP. Symmetry Propagation uses any given symmetry as a propagator, and as a result is a general symmetry breaking technique. Experiments with an implementation in the SAT solver Minisat show that on many benchmarks, Symmetry Propagation outperforms the state-of-the-art static symmetry breaking method Shatter.

Lazy clause generation is a powerful approach to reducing search in constraint programming. This is achieved by recording sets of domain restrictions that previously led to failure as new clausal propagators. Symmetry breaking approaches are also powerful methods for reducing search by recognizing that parts of the search tree are symmetric and do not need to be explored. In this paper we show how we can successfully combine symmetry breaking methods with lazy clause generation. Further, we show that the more precise nogoods generated by a lazy clause solver allow our combined approach to exploit redundancies that cannot be exploited via any previous symmetry breaking method, be it static or dynamic.