Transformation of Logical Specification into IP-formulas

Qiang Li*    Yike Guo**   Tetsuo Ida*

* Institute of Information Sciences and Electronics
  University of Tsukuba, Japan.

** Department of Computing
   Imperial College, London, U.K.

The classical algebraic modelling approach for integer programming
(IP) is not suitable for some real world IP problems, since the algebraic
formulations allow only for the description of mathematical relations,
not logical relations. In this paper, we present a language L+ for IP,
in which we write logical specification of an IP problem. L+ is a
language based on the predicate logic, but is extended with meta
predicates such as at least(m,S), where m is a non-negative
integer, meaning that at least m predicates in the set S of
formulas hold. The meta predicates are introduced to facilitate
reasoning about a model of an IP problem rigorously and
logically. Using Mathematica, we can represent the logical formulas,
called L+ formulas efficiently and completely. But the L+ formulas can
not directly executed by IP solvers. So, we need to translate L+ formulas
into a set of mathematical formulas, called IP-formulas, which most of
existing IP solvers accept.  With Mathematica, we define a set of
transformation rules and transform L+ formulas into IP-formulas and
finally simplify the IP-formulas in Mathematica. We implement the
transformation algorithm in Mathematica 3.0. Also, by using Mathlink
and CGI programming, we develop a Web-based interface to support the
system with modelling language, transformation of IP, and IP
solvers. This provides a Web-based client-server model, in which the
power of high level IP modelling and high performance IP solving can
be integrated and developed for a wide range of business users to
solve large scale decision making problems. The primary experiment
indicates that Mathematica is powerful for representing logical
formulas and for the transformation of formulas and that Mathlink is
convenient for connecting Mathematica to other software platforms.