CFLP: a Mathematica Implementation of a Distributed Constraint Solving System

Mircea (Marin^1)       Tetsuo (Ida^1)       Wolfgang (Schreiner^2)

The need for combining and making cooperate various constraint solvers is widely recognized. Such an integrated system would allow solving problems that can not be solved by a single solver. 
CFLP (Constraint Functional Logic Programming System) is a distributed software system consisting of a functional logic programming interpreter running on one machine and a number of constraint solving engines running on other machines. The interpreter is based on a deterministic version of a lazy narrowing calculus which was extended in two main directions: (a) the possibility to specify explicit OR-parallelism, and (b) the possibility to specify constraints over various domains. The OR-parallel features of the interpreter allow the decomposition of the solution space into different subspaces denoted by various sets of constraints; the individual sets are solved by different constraint solving engines in parallel and joined together to form the total solution set. This allows to investigate problems with large solution spaces using the computational power available in large computer networks.
The CFLP system is written entirely in Mathematica and uses the MathLink protocol for interprocess communication. The current implementation can solve problems expressible in functional logic and involving constraints such as systems of linear, polynomial, differential equations, and equations with invertible functions.

Introduction

Recent refinements of lazy narrowing calculi for solving equations over the domain of terms lead to successful implementations that can be used as starting point of developing a system based on equational reasoning. However, there are many applications such as theorem proving and computational geometry, where the expressive power of pure functional logic programming is not sufficient. These problems usually involve solving systems of constraint over various, like polynomial equations, differential equations, linear equations and inequations. The CLP scheme proposed by Jaffar and Lassez [JL:87] showed the possibility to integrate constraint solving capabilities over domains like reals, booleans, finite domains, rational and infinite trees in logic programming languages. Notably, almost all of these languages have a sequential implementation. Our investigation showed that it is possible to refine a lazy narrowing calculus with inference rules for handling constraints, and to develop a model for solving the constraints in a distributed environment. 
The system is called CFLP (Constraint Functional Logic Programming System) [MIS:99a] and consists of a functional logic interpreter based on a higher-order lazy narrowing calculus and a number of constraint solvers that may run on possibly different machines. The interpreter is implemented in Mathematica. The cooperation between interpreter and constraint solvers is coordinated by a constraint scheduler which schedules the individual constraint solvers to handle the solving tasks generated by the interpreter.
The paper is structured as follows. First, we illustrate by examples the system capabilities. Next, we describe the system architecture. The following subsections describe the three main components of the system: interpreter, scheduler, and constraint solvers. Finally, we draw some conclusions and directions of further research.

Examples

CFLP is delivered as a collection of Mathematica packages which add solving power to a normal Mathematica session. If CFLP is properly installed, a Mathematica user can enable it by loading the package TSolve.m

<< TSolve.m

In this section we illustrate the functionality of CFLP with a few examples.

A Polynomial Approximation Problem

Consider the problem of finding the relationship between the coefficients of a uni-variate polynomial f∈C[x] of degree 3 and a uni-variate polynomial g∈C[x] of degree 4 related by the constraint that they have the same values for x = 1,2,3,4. 
In CFLP, the polynomial f of degree 3 can be specified by the λ-term  λ[{x}, a (x^3)+b (x^2)+c x + d]  where a, b, c, d are constants,  and the polynomial g of degree 4 can be specified by the λ-term  λ[{x},m (x^4)+n (x^3)+p (x^2)+q x + r] where m, n, p, q, r are variables whose values have to be computed from the conditions

f[1] == g[1], f[2] == g[2], f[3] == g[3], 
    f[4] == g[4]

which can be specified in the compact form

map[f, {1, 2, 3, 4}]==map[g, {1, 2, 3, 4}]

where map[ f, list ] applies f to each element of list. In CFLP, map can be specified via the following functional logic program:

\(\(Prog = {
map[
              F\+_, {}] → {}, 
map[
              F\+_, \([H\+_ | Tl\+_]\)] → \([F[H] | 
                map[F, Tl]]\)};\)\)

The underlined symbols denote the free variables in the rewrite rules, and [H | Tl ] denotes a list with head H and tail Tl.
To solve equation (1), we call

\(TSolve[
      map[λ[{x}, a\ \ x\^3 + b\ x\^2\  + \ c\ x + d], {1, 2, 3, 
            4}] ≐ 
        map[λ[{x}, m\ x\^4 + n\ x\^3 + p\ x\^2\  + \ q\ x + r], {1, 
            2, 3, 4}], 
{a, b, c, 
        d}, {}, 
DefinedSymbol -> {map ∶ \((Float → Float)\)\[Cross]TyList[Float] → 
              TyList[Float], 
          f ∶ 
            Float → 
              Float}, 
Rules -> {map[
              F\+_, {}] → {}, 
          map[F\+_, \([H\+_ | Tl\+_]\)] → \([F[H] | 
                map[F, Tl]]\)}, 
Constructor -> {m ∶ Float, n ∶ Float, p ∶ Float, q ∶ Float, 
          r ∶ Float}]\)

The equational symbol ≐ denotes strict equality, i.e., the fact that the values of the two sides of the equation coincide. We identify the value of an expression with the result of rewriting it to an expression without defined symbols. 
The syntax call of TSolve is similar to the syntax call of Solve. The first 3 arguments specify the goal to be solved, the main variables of the goal, and the eliminable variables of the goal respectively. In addition, the user of CFLP can control the behavior of the computation through various TSolve options. In this example, the options are:

DefinedSymbol: the list of type–annotated symbols defined by the user,
Rules: the list of definitions for the user-defined symbols (the functional logic program),
Constructor: the list of type–annotated data constructors.

The constant coefficients of f are given as data constructors, and the unknown coefficients of g are given as main variables.
CFLP returns the unique solution:

{d -> -24 m + r, 
      c -> 
        15 m + 7 n - (7/6) (60 m + 6 n) + 3 p - 
          (3/2) (50 m + 12 n - 2 (60 m + 6 n) + 2 p) + q, 
      b -> (1/2) (50 m + 12 n - 2 (60 m + 6 n) + 2 p), 
      a -> (1/6) (60 m + 6 n)}

Note the use of higher-order variables and λ-abstractions in the specification of the goal and functional logic program. CFLP is able to handle equations involving operators defined outside the functional logic program. Furthermore, the computed answer is parametric, since r is a variable.

Electrical Circuits

This example illustrates the expressive power of the functional logic programming style extended with higher-order constructs (function variables and λ-abstractions) and capabilities to solve differential equations, linear equations, and systems of polynomial equations. We consider the problem of modelling the behavior in time of electrical circuits  built from serial and parallel connections of elementary components such as resistors, inductors and capacitors. 
First we introduce a new type constructor ElComp with associated data types res, ind, cap, serial and parallel to specify the characteristics of the electrical circuits. E.g., a resistor with resistance R=2 is specified as res[2], a serial connection of two resistors R1 and R2  is specified as serial[{res[R1],res[R2]}], and a parallel connection of a capacitor C and an inductor L is specified as parallel[{cap[C],ind[L]}]. The keyword TyList is the CFLP type constructor for lists.

TypeConstructor[
      ElComp = res[Float] | ind[Float] | cap[Float] | 
          serial[TyList[ElComp]] | parallel[TyList[ElComp]]]

Next, we define a function spec which describes the behavior in time t of an electrical component as a function of current i[ t ] and voltage v[ t ] in the circuit. The CFLP definition of spec is recursive, where the base case describes the behavior in time of the elementary circuits (resistor, inductor, capacitor) and the inductive case describes the behavior in time of serial and parallel connections of electrical components.

The CFLP program is given below. We do not explain the underlying electronic laws since it should be easy to read them off from the program.

\(Prog = 
{spec[
                res[r\+_], \(v : Float → Float\)\+_, \(i : Float → Float\)\+_] → 
              True ⇐ {λ[{t}, 
                    v[t]] ≈ λ[{t}, 
                    r\ i[t]]}, 
spec[
                ind[l\+_], \(v : Float → Float\)\+_, \(i : Float → Float\)\+_] → 
              True ⇐ λ[{t}, 
                  v[t]] ≈ λ[{t}, 
                  l\ \(i'\)[t]], 
spec[
                cap[c\+_], \(v : Float → Float\)\+_, \(i : Float → Float\)\+_] → 
              True ⇐ λ[{t}, 
                  i[t]] ≈ λ[{t}, 
                  c\ \(v'\)[t]], 
spec[
                serial[{}], λ[{t}, 
                  0], \(i : Float → Float\)\+_] → 
              True, 
spec[
                serial[\([comp\+_ | 
                      T\+_]\)], 
\(v : Float → Float\)\+_, \(i : Float → Float\)\+_] → 
              True ⇐ 
{spec[comp, v1\+_, 
                    i] ≈ 
                  True, 
spec[serial[T], v2\+_, 
                    i] ≈ 
                  True, λ[{t}, v[t]] == λ[{t}, 
                    v1[t] + v2[t]]}, 
spec[parallel[{}], 
                v\+_, λ[{t}, 0]] → 
              True, 
spec[parallel[\([comp\+_ | T\+_]\)], 
                v\+_, i\+_] → 
              True ⇐ 
{spec[comp, v\+_, 
                    i1\+_] ≈ 
                  True, 
spec[parallel[T], v\+_, 
                    i2\+_] ≈ 
                  True, 
λ[{t}, 
                    i[t]] == λ[{t}, i1[t] + i2[t]]}};\)

Consider the problem of finding the behavior in time of the current in an RLC circuit, under the restriction that the voltage is constant in time and the current was initially set to 0.

In this case, the goal which we want to solve is

G = {i[0] == 0, 
          spec[serial[{res[R0], ind[L0], 
                  cap[C0]}], λ[{t ∶ Float}, 
                V], λ[{t ∶ Float}, i[t]]] ≐ 
            True};

in variable i, and R0, L0, C0 and V are data constructors which denote arbitrary but fixed characteristic values for the resistor, inductor, capacitor and voltage of the circuit. 
Now we can ask CFLP to solve the problem:

TSolve[
      G, {i ∶ 
          Float → 
            Float}, {}, 
Rules -> 
        Prog, 
Constructor -> {R0 ∶ Float, 
          L0 ∶ Float, C0 ∶ Float, 
          V ∶ 
            Float}, 
DefinedSymbol -> {spec ∶ 
            ElComp\[Cross](Float → 
                    Float)\[Cross](Float → 
                    Float) → Bool}]

The system computes the parametric solution

\({i -> λt . e\^\(\(\((\(-\@C0\)\ R0 - \@\(\(-4\)\ L0 + C0\ R0\^2\))\)\ t\)\/\(2\ \@C0\ L0\)\)\ "C1"\_1 - e\^\(\(\((\(-\@C0\)\ R0 + \@\(\(-4\)\ L0 + C0\ R0\^2\))\)\ t\)\/\(2\ \@C0\ L0\)\)\ "C1"\_1}\)

which is represented in Mathematica by

Note the usage of type annotations in the goal, list of variables, and options of the TSolve call; CFLP has integrated a polymorphic type checker to verify the type consistency of the program and goal provided by the user.

A Problem Involving Solver Cooperation

Consider the following program

<< TSolve.m

\(Prog = {f[\(X : Compl\)\+_] → 
          g[\(Y : Compl\)\+_] ⇐ \((X + Y == 3 ∨ 
              X\^2 - Y == 9)\)}\)

in complex variables X, Y, and the goal

G = {f[X] ≈ g[Y], 
        g[(Y^2)] ≈ 
          g[(Z^2) - 1], λ[{x ∶ Compl}, H'[
              x]] == λ[{x ∶ Compl}, Z (x^Y)], H'[
            1] == 4}

with indeterminates X,H,Y,Z. In this example, the operator ∨ denotes logical disjunction, and it can be used in goals and conditional parts of rewrite rules to express alternative solutions.

Solving this goal requires a cooperation among solvers for linear, polynomial and differential equations over the domain of complex numbers. To solve G, we call:

TSolve[
      G, {X, H, Y, Z}, {}, 
Rules -> 
        Prog, 
DefinedSymbol -> {f ∶ 
            Compl → 
              Compl}, 
Constructor -> {g ∶ 
            Compl → Compl}]

In this case, the solutions computed by CFLP are parametric, and the system has generated the auxiliary variables (Subscript[C1, 7]), (Subscript[C1, 8]), (Subscript[C1, 9]), (Subscript[C1, 10]), (Subscript[C1, 11]), (Subscript[C1, 12]) to express them. It is not hard to see that these are all the solutions of G.

The Structure of the System

CFLP is a distributed software system for solving systems of equational goals in theories that can be represented as sets of conditional rewrite rules over a term algebra whose signature is extended with external operators. The external operators are used for expressing constraints over various domains.
The system consists of 3 components:

– an interpreter based on a higher-order lazy narrowing calculus C
– a cooperative constraint solver consisting of
	– a scheduler which implements a strategy S for solver cooperation,
	– various specialized constraint solvers.

The general architecture of the system is depicted below.

The Interpreter

The CFLP interpreter is designed to solve systems of equations between simply-typed λ-terms in theories axiomatized by finite sets of conditional rewrite rules of a certain kind, called pattern rewrite rules. 
Roughly speaking, simply-typed λ-terms are analogous to the Function construct of Mathematica, modulo the following differences: 

1. the keyword Function is replaced with the keyword λ,
2. each such construct (which we will henceforth call a λ-term) should be well-typed, i.e. a type can be inferred from the types of its base components (variables, constants, and function symbols).

The current version of CFLP recognizes the following base types:

({{Type, literals}, {Int, Integer literals of Mathematica}, {Float, Real literals of Mathematica}, {Compl, Complex literals of Mathematica}, {String, String literals of Mathematica}, {Bool, True,  False}})

and the following constructed types:

({{\(τ\_1×…×τ\_n → τ\), type of functions with n arguments of}, { , types (Subscript[τ, 1]), …, (Subscript[τ, n]),  
          and result of type τ}, {TyList[τ], \(type\ of\ lists\ with\ elements\ of\ type\ τ\)}})

For lists, we have adopted both the Mathematica notation {(Subscript[a, 1]),…,(Subscript[a, n])} to represent a list with elements (Subscript[a, 1]),…,(Subscript[a, n]), and the Prolog-like notation [ H | T ] to represent a list with head H and tail T.

The CFLP interpreter is based on a higher-order lazy narrowing calculus C for pattern rewrite systems [MIS:99b] extended to handle also conditional pattern rewrite systems [Pre:98]. The underlying calculus essentially consists of the unification rules of higher-order patterns [Nip:93] and the lazy narrowing rules. Since the search space of such a calculus is extremely large, we have implemented a couple of refinements with smaller search space for solutions, which are sound and complete for classes of functional logic programs which are of practical interest.
We have extended these calculi in two main directions:

(a) the possibility to specify constraints, i.e., equations that can not be solved by narrowing, but for which specialized solvers are available, and

(b) the possibility to specify explicit OR-parallelism.

The interpreter successively decomposes the goal towards an answer substitution by applying  the inference steps of the underlying lazy narrowing calculus. The only equations which can not be solved in this way are the constraints. The constraints generated upon derivations are collected and sent to be solved by specialized constraint solvers via the component called scheduler (see Fig. 1).

Note that the nondeterministic selection of a rewrite rule for a defined symbol and the explicit OR-formulas cause the initial goal to be reduced to disjoint sets of constraints that can be solved in parallel. E.g., in the last illustrative example, the reduction of the initial goal

f[X] ≈ g[Y], 
    g[(Y^2)] ≈ 
      g[(Z^2) - 1], λ[{x ∶ Compl}, H'[
          x]] ≈ λ[{x ∶ Compl}, Z (x^Y)], H'[
        1] == 4

involves the decomposition of the equation f[X]≈g[Y] into simpler equations. The transformation step performed by our lazy narrowing calculus is:

f[X] ≈ g[Y] ⇒ X ≈ X0, 
    g[Y0] ≈ 
      g[Y], (X0 + Y0 == 3 ∨ 
        (X0^2) - Y0 == 9)

where X0,Y0 are new variables. In this step we have used the fresh variant

f[X0] -> 
      g[Y0] ⇐ (X0 + Y0 == 3 ∨ 
            (X0^2) - Y0 == 9)

of the rewrite rule which defines f.

During step (2), an OR-subgoal is produced and as a result the initial goal is finally decomposed in two disjoint sets of constraints. These sets of constraints are sent to be solved to the scheduler.

The Scheduler

The scheduler coordinates the process of solving the systems of constraints received from the interpreter. In order to solve these sets of constraints, the constraint scheduler maintains a dynamic data structure called a constraint tree. The nodes of the constraint tree are pairs of the form ⟨θ,cs⟩ where θ is a substitution and cs is a set of constraints.
Whenever a set of constraints cs is received from the interpreter, the scheduler adds a new son ⟨ϵ,cs⟩ to the root of the constraint tree. Here ϵ stands for the empty substitution. The scheduler expands this tree by applying constraint solving methods in parallel to its leaf nodes. 
A leaf node ⟨θ,cs⟩ is expanded w.r.t. a method m as follows:

1) cs is decomposed into a set (Subscript[cs, 1]) of constraints to which method m can be applied, and a set (Subscript[cs, 2]) of other constraints.

2) (Subscript[cs, 1]) is sent to be solved to a constraint solver which implements method m. We call such a solver an m-solver.

3) If the m–solver detects (Subscript[cs, 1]) inconsistent then the node ⟨θ,cs⟩ is marked as inconsistent. Otherwise the m-solver returns ⟨ϵ,cs⟩ if it can not reduce (Subscript[cs, 1]), or it computes a finite sequence of pairs ⟨(Subscript[θ, 1]), \(TraditionalForm\`\(cs\_1\%, \)\) ⟩,…,⟨(Subscript[θ, p]), \(TraditionalForm\`\(cs\_p\%, \)\) ⟩ with the property that θ is a solution of cs iff there exists a solution (Subscript[σ, i]) of some \(TraditionalForm\`\(cs\_i\%, \)\) (1≤i≤p) such that θ = (Subscript[θ, i])(Subscript[σ, i]).

4) If the sequence ⟨(Subscript[θ, 1]), \(TraditionalForm\`\(cs\_1\%, \)\) ⟩,…,⟨(Subscript[θ, p]), \(TraditionalForm\`\(cs\_p\%, \)\) ⟩ is computed by the m-solver, then the nodes ⟨θ (Subscript[θ, i]), (Subscript[cs, 2])(Subscript[θ, i])⋃ \(TraditionalForm\`\(cs\_i\%, \)\)⟩  (1≤i≤p) are added to the constraint tree as sons of the node ⟨θ,cs⟩.

A node ⟨θ,cs⟩ is final if it can not be reduced by any m-solver which is available.

The implementation of the scheduling algorithm is inspired by the work of Hong [Hong:94]. The scheduler can be regarded as a component parameterized with a list M={(Subscript[m, 1]),…,(Subscript[m, k])} of constraint solving methods. The scheduler implements a cooperation strategy S which repeatedly applies the sequence (Subscript[m, 1]),…,(Subscript[m, k]) of methods to the leaves of the constraint tree until they become either final or inconsistent. As soon as a final node is generated, it is made accessible to the interpreter.

The Constraint Solvers

The constraint solvers are implementations of the constraint solving methods specified to the scheduler through the list M. The current implementation of CFLP provides constraint solvers which implement the following methods for solving constraints over the domains of real and complex numbers:

1) Linear: a method for solving systems of linear equations and systems of equations with invertible functions,
2) Polynomial: a method for solving systems of polynomial equations,
3) Derivative: a method for solving derivative equations,
4) PartialDerivative: a method for solving partial derivative equations.

These methods are tried in the order presented.

All solvers are implemented by separate Mathematica processes executing in parallel and communicating with the constraint scheduler via MathLink connections. There are two types of constraint solvers in CFLP:

1) Local constraint solvers: these solvers run as subsidiary Mathematica processes of the CFLP constraint scheduler.

2) Shared constraint solvers: a shared constraint solver is started from outside a CFLP session and can be connected later to more CFLP schedulers which may run on possibly different machine.

The user can adjust the distributed constraint solving component of the system by specifying the number of local constraint solvers which are started at system initialization, and the remote machines on which to look for shared constraint solvers.
The communication mechanism between scheduler and constraint solvers is implemented completely in MathLink [Wol:96]. Therefore, CFLP is a platform-independent software system and can be used in heterogeneous networks.

Conclusion and Future Work

CFLP is a software system consisting of a functional logic interpreter and a distributed constraint solving system, which provides support for solving systems of equations over various constraint domains. The functional logic component allows to define one's own abstractions in an easy and comfortable way. In the current implementation we have integrated solvers for linear equations and equations with invertible functions, polynomial equations, differential equations, and partial differential equations. The constraint solvers are all implemented on top of the constraint solving capabilities of Mathematica.

We intend to further develop the system by integrating more constraint solving capabilities. The constraint solvers may act either on disjoint sets of constraints or on overlapping subsystems. Currently, the constraint solvers are not allowed to act simultaneously on a leaf node of the constraint tree. An optimization would be to act simultaneously with more solvers on the same node in situations when the subsystems of equations are non-overlapping.

Because of the higher-order extensions of the functional logic programming framework (function variables and λ-abstractions), the search space of lazy narrowing is very large. We have identified and implemented various refinements of a lazy narrowing calculus which perform a more deterministic search for solutions for classes of functional logic programs of practical interest. We intend to continue our research and identify better refinements.

The system is intended to be used by researchers in functional and logic programming languages, and by researchers in constraint solving who are willing to make use of its expressive and computational power.

References

[Hong:94] H. Hong. RISC-CLP(CF): Constraint Logic Programming over Complex Functions. In F. Pfennig (ed.): Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, LPAR'94, pp. 99-113, Springer-Verlag Berlin Heidelberg, 1994.

[JL:87] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. Technical Report. Department of Computer Science, Monash University. Clayton 1987.

[MIS:99a] M. Marin, T. Ida and W. Schreiner. A Distributed System for Solving Equational Constraints based on Lazy Narrowing Calculi. In JSSST Workshop on Programming and Programming Languages (PPL'99), Togawa, Japan, March 17-19, 1999.

[MIS:99b] M. Marin, T. Ida and T. Suzuki. On Reducing the Search Space of Higher-Order Lazy Narrowing. In A. Middeldorp, T. Sato (eds.): FLOPS'99, LNCS 1722, pp.319-334, November 1999. Springer-Verlag Berlin Heidelberg, 1999.

[Nip:93] T. Nipkow. Functional Unification of Higher-order Patterns. In Proceedings of the 8th IEEE Symposium on Logic in Computer Science, pp.64-74, 1993.

[Pre:98] C. Prehofer. Solving Higher-order equations. From Logic to Programming. Birkhäuser Boston, 1998.

[Wol:98] S. Wolfram. The Mathematica Book. Third Edition. Wolfram Media and Cambridge University Press, 1996.