Abstract: This paper presents a new approach for exactly solving the Unbounded Knapsack Problem (UKP) and proposes a new bound that was proved to dominate the previous bounds on a special class of UKP instances. Integrating bounds within the framework of sparse dynamic programming led to the creation of an efficient and robust hybrid algorithm, called EDUK2. This algorithm takes advantage of the majority of the known properties of UKP, particularly the diverse dominance relations and the important periodicity property. Extensive computational results show that, in all but a very few cases, EDUK2 significantly outperforms both MTU2 and EDUK, the currently available UKP solvers, as well the well-known general purpose mathematical programming optimizer CPLEX of ILOG. These experimental results demonstrate that the class of hard UKP instances needs to be redefined, and the authors offer their insights into the creation of such instances.
Abstract: This paper addresses the issue of state sharing in CSPï¿¿B specifications: B machines controlled by various CSP parts are supposed not to refer to, share or modify the same state space. However, some kinds of B state sharing can be allowed without creating inconsistencies in CSP||B specifications. To achieve this, we present a B-based solution for allowing architectures with B state sharing in the CSP||B components. We show that the inconsistencies in state sharing can be identified by translating the CSP controllers into B specifications and then using a more refined consistency checking process. We also hint at possible ex- tensions towards other CSP||B architectural patterns with various types of sub-components sharing.
Abstract: FROST (Fold Recognition-Oriented Search Tool) is a
software whose purpose is to assign a 3D structure to a protein
sequence. It is based on a series of filters and uses a database
of about 1200 known 3D structures, each one associated with
empirically determined score distributions. FROST uses these
distributions to normalize the score obtained when a protein sequence is
aligned with a particular 3D structure. Computing these distributions
is extremely time consuming; it requires solving about $1,200,000$
hard combinatorial optimization problems and takes about 40 days on a
2.4~GHz computer. This paper describes how FROST has been
successfully redesigned and structured in modules and independent
tasks. The new package organization allows these tasks to be
distributed and executed in parallel using a centralized dynamic load
balancing strategy. On a cluster of 12 PCs, computing the score
distributions takes now about 3 days which represents a parallelization
efficiency of about 1.
Abstract: In this paper, we use integer programming approach for solving a hard combinatorial optimization problem, namely protein threading problem. For this sequence-to-structure alignment problem we apply
cost-splitting technique to derive a new Lagrangian dual formulation.
The optimal solution of the dual is sought by an algorithm of a polynomial complexity. For most
of the instances the dual solution provides an optimal or near-optimal (with negligible duality gap)
alignment. The speed-up with respect to the broadly advertised approach for solving the
same problem is from 100 to 250 on computationally interesting instances.
Such a performance turns computing score distributions, the heaviest task when solving PTP, into a routine operation.
Abstract: Among the possible approaches for expressing real-time problems with the \B\
method, two are dominant : the use of the usual \B\ mechanisms to define
temporal constraints on the one hand, and extending \B\ through another
formalism more adapted to the real-time context on the other hand.
We define here a possible temporal semantic for \B, by using a temporal
logic (the duration calculus), and we illustrate how this extension affects
the proof mechanism used to show the soundness of abstract machines.
Abstract: In this paper, we present a new approach to
generating different codes from specifications developped with the B
method. This code generator is based on the flattening algorithm
and the use of a rewriting tool (an XSLT processor, for example).
Currently, the commercial code generation processors are black box
tools, and it is very difficult to modify them. We will show that
our approach simplifies code generation specification, which makes
the specification of new code generators for new target languages
easier and faster. Another benefit of our approach is that it
allows assertions to be added to the code generated. Assertions,
are expressed in the specifications but they are forgot in the
current code generation process
