Operation 2 : Solving of geometric constraints

Head : Pascal Schreck PR1

Participants : Gabriel Braun AP associated in 2009, Caroline Essert AP, Pascal Mathis AP, Julien Narboux AP

Ph.D. candidates : Claire Baegert, Simon E.B. Thierry

Presentation of the domain

The general question that subtends this operation consists in the automatic output of geometric objects defined by a specification expressed in the adequate language. This question is obviously very (too¹ !) general. In our case we have reduced the problem to the context of geometry and, as the field still remains wide, we have declined it in several distinct problems. Thus, starting from the automatic solving of geometric construction problems by ruler and compass - where the problem is given literally, without numerical data, and where the result takes the form of a construction program - we have studied two other problems which are very different :

the solving of geometric constraints related to CAD where the problem is set as a sketch and the solution is the digital geometric figure which, from one side, satisfies the measurement system constraints, and from the other side, looks as close as possible to the sketch;

the trajectory planning of a needle (or more generally of a system supporting a necrosis mechanism) allowing the removal of a hepatic tumor by radio-frequency ; the problem is set as a 3D reconstruction of the patient's organs, patient-specific data and possibly data from the practitioner and the solution is a set of needle positions.

Constructions by ruler and compass

Constructions by ruler and compass have a long history in mathematics and are more often known as one of the first illustrations of Gallois theory. Despite having studied this question - in particular by implementing Lebesgue's method [4-SCH03] - we focused more on its purely geometric aspect by targeting the field of computer-aided teaching. We have thus highlighted the logical aspects by linking with automatic proofs of theorems.

The ideas set up in this context allowed to realize a prototype written in Prolog, but above all they allowed to output a certain style of approach of constraints solving borrowing to logics, abstract algebraic specifications and software engineering in order to conciliate the underlying theoretical ideas with the software production modeling the problem [4-SCH01].

Constructions vs proofs

The domains of solving of geometric constraints on one side and automatic proofing in geometry on the other side are closely related; indeed:

for the solving of geometric constraints it is necessary to prove (at least implicitly) geometrical theorems,
the methods of automatic proofing in geometry (Wu, area's method, ...) assume that the problem is presented as a construction by ruler and compass.

Starting from this observation we jointly work on the formalization of the notion of geometric construction and the formalization of automatic proofing techniques within the proofing assistant Coq. Representing these notions in a formal and unique fashion will allow us to guarantee both the correction of the proposed algorithms (in particular the treatment of degenerate cases, see Operation 3) and the combination of automatic proofing methods with algorithms of constraints solving.

Solving of geometric constraints

It is in the above mentioned spirit that we have approached, with Jean-François Dufourd, the problem of solving of constraints systems coming from CAD sketches (thesis of Pascal Mathis, 1998). This problem is quite different from the constructions by ruler and compass not only in the way of setting the problem to solve but also in the nature of the expected result : a digital figure which in an approximated solution of the measurements system. This simplification in the nature of the result but also in the importance of the problem in industry, or simply in other scientific fields, have favored the appearance and study of very different approaches. Among them we can cite the methods of numerical solving of systems of equations (Newton-Raphson's method, continuation method or interval arithmetic), and graph-based methods issued from the theory of rigidity. We have shown that the approaches based on a formalization of geometry in the style of constructions by ruler and compass are also competitive.

Another feature of CAD related constraints systems is their displacement invariance. This feature has been exploited by numerous approaches in order to decompose the constraints systems in sub-systems. We have given, from our side, a formal framework to this invariance phenomenon which allowed us to develop a multi-agent architecture based solver in order to make several local servers (formal or digital) collaborate. This study also allowed us to extend the question to constraints systems invariant by other groups (typically the similarity group [2-SS06]) but also to consider invariance groups for sub-systems [2-SM06]. The formalization of geometric constraints systems has also allowed to prove the correctness of decomposition methods [2-MT09]. Our most recent studies in this field are about the extensions of geometric decomposition tools in the continuation of previous work. Thus we decided to study :

on one side, the systematical study of the system's sub-constraint nature by the study of their invariance group (thesis of Simon E.B. Thierry) thus offering a unified framework for solvers and articulated mechanism simulators [4-TMS07] ;

on the other side, the notion of quasi-decomposability where we authorize ourselves to replace the constraints by others changing then the structure of the constraints system. This approach [4-FS07] requires the cooperation of formal solvers - which produce a construction plan - and numerical solvers which use the generated construction plan in order to numerically compensate the constraints (thesis of Arnaud Fabre, 2006).

In all these works we have been using a high-level of parameterization software framework : we placed ourselves at the meta level in order to more easily describe the geometric universes in which the solvers take place. Our goal being to facilitate the insertion of solvers in a multi-agents system, facilitate the experimentation of conceivable geometric modeling, and to allow a unified benchmark description. For this purpose we have conceived a description language (GCML) based on XML, and tools allowing to exploit the descriptions written in this language (master's thesis of Julien Wintz and thesis of Arnaud Fabre, see also 4-WSM06]).

Ablation planning by radio-frequency

Geometric constraints do not only come from computer-aided teaching or CAD. The problem of planning of thermal ablation of tumors is a new topic where we test our ideas (postdoc of Caroline Essert, thesis of Claire Baegert). The different techniques of thermal ablation that exist (radio-frequency, cryoablation, radiotherapy, etc.) share the same principle and have numerous common points. It consists in all cases to burn the whole tumor to avoid recursion and at the same time avoiding to damage sound tissues or surrounding organs. Each technique has of course its specificities, both on the intervention mode or its effects.

The goal of this work has thus a unique target: plan the surgery for a given patient and technique by offering the practitioner an optimal intervention scenario and by predicting the effects. Therefore we are aiming at elaborating methods issued from constrained geometric calculus [4-VBS05].

The used geometric constraints are a formalization of the given problem and of the knowledge coming from the surgeon's expertise applied to a 3D model of the patient. Our recent advances on this theme has enabled us to decompose the constraints in two classes:

the strict constraints, or boolean, which inevitably need to be satisfied [4-BVS07a] ;

the soft constraints, which are often numerical constraints to be satisfied as best [2-BVS07].

The solving of these constraints goes through an elimination step of the solutions which do not satisfy the entirety of the strict constraints, and then through a second step which tunes the possible solutions by optimizing the soft constraints.

Finally, interactivity is offered (see Operation 5) to allow the practitioner to :

test other possibilities ;
tune the parameters (weight of each soft constraint, etc.).

We are currently studying ways for adding new constraints in the system by the practitioner by locating at a meta level description. We focus on genericity in order to allow an eased extension of the planning system to other surgical operations [4-EBS09].

This genericity is currently studied via the extension of the planning system to interventions of neurosurgery (placement of deep brain stimulation electrodes, glioma removal). This work is operated in collaboration with the research group Visages at INRIA Rennes Bretagne Atlantique and Dr. Haegelen and Pr. Morandi from CHU Rennes. Also we plan on extending this work to cryoablation planning by soliciting the implementation of several simultaneous effectors in interaction. This work will be conducted in cooperation with the group of Pr. Gangi from CHU Strasbourg.

Notes

1 - this is the typical problem of undecidable prototype and we know since the 70's that the idea of a "universal solver" - inevitably incomplete, but nevertheless capable of apprehending very diverse problems - is a pure illusion.

Theme 1 operation2

Contents