Descripción: This paper presents a new generalization of the graph multicoloring problem. We propose a Branch-and-Cut algorithm based on a new integer programming formulation. The cuts used are valid inequalities that we could identify to the polytope associated with the model. The Branch-and-Cut system includes separation heuristics for the valid inequalities, specific initial and primal heuristics, branching and pruning rules. We report on computational experience with random instances. © 2009 Elsevier B.V. All rights reserved.

Descripción: The Traveling Deliveryman Problem is a generalization of the Minimum Cost Hamiltonian Path Problem where the starting vertex of the path, i.e. a depot vertex, is fixed in advance and the cost associated with a Hamiltonian path equals the sum of the costs for the layers of paths (along the Hamiltonian path) going from the depot vertex to each of the remaining vertices. In this paper, we propose a new Integer Programming formulation for the problem and computationally evaluate the strength of its Linear Programming relaxation. Computational results are also presented for a cutting plane algorithm that uses a number of valid inequalities associated with the proposed formulation. Some of these inequalities are shown to be facet defining for the convex hull of feasible solutions to that formulation. These inequalities proved very effective when used to reinforce Linear Programming relaxation bounds, at the nodes of a Branch and Bound enumeration tree. © 2008 Elsevier B.V. All rights reserved.

Descripción: The theory of dynamic frames is a promising approach to handle the so-called framing problem, that is, giving a precise characterizations of the locations in the heap that a procedure may modify. In this paper, we show that the machinery used for dynamic frames may be exploited even further. In particular, we use it to check that implementations of abstract data types maintain certain structural invariants that are very hard to express with usual means, including being acyclic (like non-circular linked lists and trees) and having a unique path between nodes (like in a tree). The idea is that regions in this formalism over-approximate the set of reachable objects. We can then maintain this structural invariants by including special preconditions in assignments, of the kind that can be verified by state-of-the-art SMT-based tools. To test this approach we modified the verifier for the Dafny programming language in a suitable way and were able to enforce these invariants in non-trivial examples. © 2011 Springer-Verlag.