Khalid Al-Ali
email: kalali@masdar.ac.ae

SOLAR UPGRADE OF METHANE USING DRY REFORMING IN DIRECT CONTACT BUBBLE REACTOR

Keywords: Direct Contact Bubble Reactor, Solar Reformer, Methane Dry Reforming, Solar energy conversion, Methane Up-gradation

The reforming behavior of a direct contact bubbling CH 4 -CO 2 mixture, was quantitatively investigated, in an alkali carbonate based molten salt system containing suspended Ni-Al 2 O 3 catalyst. A thermodynamical process of a solar reformer of dry methane reforming was proposed to operate in a temperature range of 600-800 o C. The selectivity of the thermal fluid have been validated according to specific requirements including lower melting point, thermal and chemical stability, acting simultaneously as heat transport and sensible heat storage. A ternary mixture of alkali carbonates system Na 2 CO 3 , K 2 CO 3 and Li 2 CO 3 of ratio 1:2:2 fulfills our requirements for the direct contact bubble reactor of the solar reformer, in which a CO 2 -rich mixture of methane was reformed to produce synthesis gas. The reforming behavior was experimentally investigated to quantify the product compositions, pursuing to maximize the methane conversion and H 2 yield, while minimizing coke depositions and carbonization effects. Three types of Ni-loading (10%, 15% & 20 wt. %) -Al 2 O 3 catalysts were prepared by impregnation using nickel nitrate solution. The results exhibited that 15%Ni-Al 2 O 3 catalyst showed the highest activity and selectivity with respect to H 2 % yield (or H 2 :CO production ratio) and carbon deposition rates. The thermodynamic analysis showed the positive effect of excess CO 2 on the process of dry CH 4 reforming in alkali carbonate salts; the higher CO 2 /CH 4 ratio, the lower reaction temperature can be achieved; subsequently, minimizing the thermal decomposition of alkali carbonates. However, the experimental results expressed the increase of CO 2 /CH 4 ratio in terms of higher methane conversion, whereas the H 2 :CO production ratio was significantly decreasing, attributed to increase in water formation as a result of Reverse Water Gas Shift (RWGS) reaction. While, the carbon deposition is decreasing as per the theoretical results.

Introduction

The global directive into the development and utilization of the abundant solar energy, which results in no any or little pollution, is not only an urgent supplementary to the energy in the present stage, but also a foundation of energy structure in the future. It compels to deeply look at the efficient solar energy utilization and to examine the challenges and opportunities for the development of solar energy utilization as a competitive energy source. Solar fuels are part of the solution, they have the capacity to help satisfy the energy needs of the world without destroying it [START_REF] Meier | Solar Fuels from Concentrated Sunlight[END_REF][START_REF] Momirlan | Recent direction of world hydrogen production[END_REF] The conversion of solar energy into chemical energy carriers overcomes the main drawbacks of solar energy, namely: it low spatial density, its intermittent, and its inconvenient distribution [START_REF] Crabtree | Solar energy conversion[END_REF]. Solar fuels, such as hydrogen, can be produced from upgrading fossil fuels. CO 2 reforming of natural gas (methane) is highly endothermic, catalytic process, which produces syngas (CO and H 2 ) [START_REF] Wang | Carbon Dioxide Reforming of Methane To Produce Synthesis Gas over Metal-Supported Catalysts: State of the Art[END_REF].

𝐶𝐻 4 + 𝐶𝑂 2 → 2𝐶𝑂 + 2𝐻 2 ∆𝐻 @ 298𝐾 𝑜 = +247 𝐾𝐽/𝑚𝑜𝑙 (1)
Reaction enthalpy of the reformed product is larger than fuel source, hence heat output of fuel is enhanced. The challenge is to produce large amounts of chemical fuels directly from sunlight in robust, cost-effective ways while minimizing the adverse effects on the environment [START_REF] Meier | Solar Fuels from Concentrated Sunlight[END_REF].

Solar reforming of methane is the most feasible technology due to both commercial and environmental reasons as; at relatively high temperature Solar Thermo-Chemical (STC) processes, the methane reforming reaction with CO 2 has a larger endothermic enthalpy per mole ∆H o than that with H 2 O, and it can be realized with STC energy conversion systems [START_REF] Gokon | Methane reforming with CO 2 in molten salt using FeO catalyst[END_REF]. CO 2 reforming of methane would result in lower H 2 /CO ratio in syngas, which is favorable to the synthesis of oxygenated compounds [START_REF] Larentis | Modeling and optimization of the combined carbon dioxide reforming and partial oxidation of natural gas[END_REF]. CO 2 Reforming process consumes two important greenhouse gases CO 2 and methane and converts them into valuable feedstock. Therefore it is of a great interest for environmental protection [START_REF] Guczi | Methane dry reforming with CO 2 : A study on surface carbon species[END_REF].

The main vector for this research will be the production of syngas from methane dry reforming, a potentially clean alternative to fossil fuels. Today, however, more than 90% of hydrogen is produced by using high temperature processes from fossil resources, mainly natural gas. If hydrogen is generated from solar energy, it is definitely a clean technology; no hazardous wastes or climate changing byproducts are formed.

Nevertheless, one of the essential problems in the solar reforming of methane is fluctuating incident solar radiation. The catalytic methane reforming with CO 2 requires stable operation under the fluctuation of insolation by a cloud passage. Moreover, the solar chemical receiver reactor to which the concentrated solar radiation is directed requires thermal uniformity inside the reactor [START_REF] Kodama | CO 2 Reforming of Methane in a Molten Carbonate Salt Bath for Use in Solar Thermochmical Processes[END_REF]. One solution to these problems is to use the concept of Direct Contact Bubble Reactor (DCBR) with molten metal salt of highly heat capacity as heat transfer medium in the solar receiver-reactor. Here, we are proposing the importance of using direct heat transfer by utilizing the conceptual idea of DCBR for methane reforming with carbon dioxide.

Furthermore, due to the absence of any intervening wall separating the processing fluids, these units of DCBRs have many advantages over the traditional shell-and-tube heat exchanger, among which one can highlight higher thermal efficiency; greater simplicity of construction, that accordingly reducing capital, operating and maintenance costs; and the possibility of economically processing highly fouling and/or corrosive solutions.

DCBR is proposed to promote solar thermal energy storage idea with higher energy conversional capacity, higher thermal efficiency, more stable operation under the fluctuation of incident solar radiation and greater simplicity of construction Despite the great advantages offered by DCBR, there are still many areas of uncertainty with respect to methane dry reforming processes with carbon dioxide, and these problems need to be solved before this application can be proceed commercially. The CH 4 -CO 2 reforming reactions are highly endothermic that possess very high energy consumption. The current catalyst is not able to achieve conversion over 80% unless in extreme temperature conditions (> 800 o C). However, the objectives of this research are; to find out the catalytic thermal fluid which is suitable for the STC methane dry reforming for converting solar high-temperature heat to chemical fuels, to investigate the reforming behavior of CH 4 with CO 2 at lower temperature ranges 600 -800 o C, and to quantify the product compositions in the selected thermal fluid of alkali carbonate based molten salt system.

Experimental and Method

Experimental Set-up

The schematic diagram of the experimental system is shown in Fig. 1. A narrow-bore cylindrical stainless steel reactor with body made of SUS-304 TP, 18 mm outer diameter, 1.5 mm thickness and 38 mm long, was used as the DCBR between the thermal fluid of alkali-metal carbonates molten salt system and the bubbling gas mixture of CH 4 , CO 2 and the carrier gas, Ar.

An alkali-metal carbonate mixture of Na 2 CO 3 , K 2 CO 3 and Li 2 CO 3 of ratio 1:2:2, was used as a molten salt bath because it shows the lowest melting point, relatively close to eutectoid melting point, and has relatively high heat capacity value. The alkali-metal salt mixture was mixed with the Al 2 O 3 -supported Ni metal catalyst at a desired weight ratio. The selection of both thermal fluid and catalyst would be explained in details in next sections. A mixture of catalyst and molten salt was placed in the reactor.

A CH 4 /CO 2 mixture of desired mole ratio was introduced through a narrow-bore stainless steel tube ∅ inner = 1mm to the bottom of the inside reactor. The flow rates of CH 4 , CO 2 and inert gas Ar were controlled by mass flow meters. The total flow rate of the mixed gases feed ranged from 75 to 200 ml/min at atmospheric pressure.

The reactor was externally heated by an infrared furnace of 0.8KW electrical power, 800 Volt and 8AMP up to 600 -800 o C within 15 -20 min . Afterward, the CH 4 / CO 2 mixture was bubbled through the molten salt-catalyst mixed bath. The temperature was controlled using K-type thermocouple in contact with the external wall of the reactor, whereas, the inside K-type thermocouple in contact with the reactive bubbling system was used to record the real endothermic reaction temperature using software controlled thermal data acquisition system E830.

The effluent gases from the reactor were introduced to silica gel, to absorb the moisture content during the reaction. The dry effluent gases were analyzed using Direct Gas Mass Spectroscopy, DGMS (BRUKER-axs Model MS 9600 -Material Analysis and Characterization)

Selection of a Thermal Fluid

Alkali metal carbonate has been widely used in coal-CO 2 gasification [START_REF] Matsunami | Coal gasification by CO 2 gas bubbling in molten salt for solar/fossil energy hybridization[END_REF] and the experimental results of Gokon et al, 2002 [START_REF] Gokon | Methane reforming with CO 2 in molten salt using FeO catalyst[END_REF] showed that the methane reforming reaction with CO 2 using FeO catalyst in the molten carbonate is useful for the conversion of solar energy into chemical energy. AO Xian-quan and WANG H. [START_REF] Ao Xian-Quan | Reduction behavior of methane in alkali molten carbonates[END_REF] studied the reduction behavior of methane cracking in alkali-metal based molten salt system. These suggest that the alkali molten carbonates mixture was one of promising molten salt for methane conversion and the most attractive thermal fluid to be applied to the solar thermochemical methane dry reforming for converting solar high-temperature heat to chemical fuels.

Mixed salts system is often used in molten salt system; the reason partly is mixed salts system generally has a low melting point, i.e. the melting points of pure salts of Li 2 CO 3 , Na 2 CO 3 and K 2 CO 3 are 618, 851 and 891, respectively. The melting point of ternary carbonate eutectic (32 wt% Li 2 CO 3 , 35 wt% K 2 CO 3 , and 33wt% Na 2 CO 3 ) starts at 397 o C [START_REF] David | Molten Salt Technology[END_REF]. Moreover, the eutectic mixture of salts has a higher stability and to remain unchanged over a wide range of chemical conditions. This because coordination can be formed between anions and cations in molten salt mixture, and mixed molten salts system has higher coordination number if compared with its pure salt [START_REF] Ao Xian-Quan | Reduction behavior of methane in alkali molten carbonates[END_REF][START_REF] David | Molten Salt Technology[END_REF] An experimental procedure have been proceeded to validate the results of mixed alkali-metal carbonates of KANTO Chemicals using Li 2 CO 3 , Na 2 CO 3 and K 2 CO 3 with purity of 99.95%, 99.97% and 99.95%, respectively. 21 data points have been decided on the ternary diagram, as shown in Fig. 2. The ternary diagram boundaries' points (P1, P2, P3, P4, P6, P7, P10, P11, P15, P16, P17, P18, P19, P20, P21) have the values of binary mixed alkali-metal carbonates system using FACTSage Database Documentation of binary phase systems, 2009, whereas the ternary points of (P5, P8, P9, P12, P13, P14) are experimentally determined using simultaneous Thermogravimetric/Differential Thermal Analysis, TG/DTA, equipment. The measured data of solidus and liquidus temperatures are summarized in Fig. 2. The Eutectic melting point usually appears where the solidus and liquidus temperatures are coinciding. Accordingly, point P9, highlighted in Fig. 2, with ternary mixture of alkali carbonates system Na 2 CO 3 , K 2 CO 3 and Li 2 CO 3 of ratio 1:2:2 reveals the closely rapprochement to the eutectic point.

Catalyst Characterization -Ni Particle size and X-ray diffraction

In order to determine the surface area of the used catalysts, the X-ray diffraction spectra were obtained with HZG-4S apparatus ,Cu-K α radiation ( λ =1. not significantly change the phase structure of the support. However, The Ni and NiO crystallite size can be estimated from the Full Width at Half Maximum (FWHM) of the their corresponding peaks using Scherrer equation. The results is given in Table 1.

Catalyst Characterization -Transmission Electronic Microscopy (TEM)

The TEM images of fresh Ni% loading of (10%, 15% & 20 -Al 2 O 3 wt.%) catalysts were taken with JSM-6510LA -Analytical Scanning Electron Microscope, as shown in Fig. 4, with magnification of × 1000, to investigate the surface morphology and crystallinity of the fresh catalysts.

Theory of Methane Conversion

Given the following real-world reaction scheme for the methane dry reforming;

CH
A c = CH 4 + CO 2 + CO + 2 C 2 H 2 + 2 C 2 H 4 + 2 C 2 H 6 (3)
B o = CO + 2 CO 2 + 2 O (4) C H = 2 H 2 + 4 CH 4 + 2 C 2 H 2 + 4 C 2 H 4 + 6 C 2 H 6 (5)
The quantities of the two unknown species of carbon black deposition and the H 2 O formation can be determined using the mole balanced equation on C, H, and O as follows;

C O = A c + C B o + H 2 O = a (6)
C H = A c + C C H +2 H 2 O = b (7)
The chemical conversion of CH 4 , is defined as the mole ratio of CH 4 decomposed to CH 4 in the feed. However, the CH 4 conversion can be defined with respect to the outlet concentrations of species as follows;

The CO 2 conversion can be defined in same manner as follow;

Conversion CO 2 % = 1 - CO 2 A c + C × m (9)
Where the values of n and m are related to intial conditions of CH 4 : CO 2 , in such that n defines the theoretical methane concentration in terms of a fraction of intial concentations of carbon contained species. Similarly, m defines the theoretical CO 2 concentration in terms of a fraction of intial concentations of carbon contained species. These values of a, b, n and m are shown in The H 2 yield, is defined as the mole ratio of H 2 in the gas products measured by DGMS to the theoretically maximum H 2 when the reaction reaches completion:

Yield H 2 % = H 2 out 2× CH 4 in × 100 ( 10
)
The CO yield is defined as;

Yield CO % = CO out CH 4 in + CO 2 in × 100 (11)
The H 2 O yield is defined as;

𝑌𝑖𝑒𝑙𝑑 𝐻 2 𝑂 % = 𝐻 2 𝑂 𝑜𝑢𝑡 2× 𝐶𝐻 4 𝑖𝑛 × 100 (12)

Results and Discussions

Influence of Nickel Loading Catalysts

The influence of Ni loading on the conversions of methane and H 2 yield at reaction temperature of 800 o C, and the flow of both CH 4 and CO 2 of ratio of 1:1 at 50 mL/min, is shown in Fig. 5, in which data was obtained after 4 hours reaction. As expected, the conversion is related to the metal loading. The methane conversion increased from 45% to 69% as the Ni % loading decreased from 20% to 10%. However, the H 2 yield exhibited the highest at Ni% loading of 15%. The catalytic activity revealed increasing during the first 4 hrs reaction and found active for CH 4 dry reforming.

Fig. 6 shows the effect of reaction temperature from 600 -800 𝑜 C on the methane conversions and H 2 yield. They were significently increased as the reaction temperature increased. The methane conversion of 15% Ni loading was nearly same as 20% Ni loading in low reaction temperatures. However, in high temperatures, the catalytic activity increased toward the highest methane conversion and hydrogen yield.

The influence of Ni% loading on the carbon deposition is illustrated in Fig. 7. 15%Ni-Al 2 O 3 catalyst showed the lowest carbon deposition in grams per mole of methane. The effect of reaction temperature on coke formation is significient at relatively high temperatures as the methane conversions (or methane cracking reactions) are the highest .

Effect of Excess 𝐶𝑂 2 on Methane Dry Reforming

The feed flow ratio of CO 2 /CH 4 was changed to 3:1, 2:1 & 1:1, at constant reaction temperature of 800 o C with constant CH 4 flow rate of 20 ml/min and constant total inlet flow rate of 100 ml/min by varying the inert Ar gas, that to avoid the effect of flow rates and residence time on methane conversion. The catalyst used is 15% Ni -Al 2 O 3 catalyst Fig. 8 illustrates the influence of excess CO 2 on methane dry reforming reaction. As the CO 2 : CH 4 ratio increased from 1:1 to 3:1, the conversion of methane increases from 73% to 89%, whereas the H 2 yield decreased from 46% to 22%. Along with the increase of methane conversion, both of H 2 O% and CO% yields are also increasing, as shown in Fig. 9.

It clearly understandable from the positive value of heat of formation of Reverse Water Gas Shift (RWGS) reaction, equation 13, which is much lower than methane dry reforming reaction, equation 1. This indicates that the side reaction of RWGS reaction takes place faster than the main reaction. In same context, it is much easier for CO 2 to react with H 2 than the deposited C, equation 14

CO 2 + H 2 → CO + H 2 O ∆H @ 298K o = +41 KJ/mol (13) CO 2 + C → 2CO ∆H @ 298K o = +172 KJ/mol (14)
As a result, the H 2 (desire product) formed from the methane dry reforming process will react immediately with CO 2 to produce H 2 O (undesired product) and directly reduces the overall H 2 yield and increases CO yield. This is in full agreement with experimental laboratory results in which have showed that CO 2 conversion was higher than that of CH 4 ; higher CO yield compared to H 2 yield; and CO: H 2 ratio was increasing as CO 2 : CH 4 ratio increased. Therefore, the understanding of the effect of water formation from side reactions is important as to determine the optimum conditions in order to avoid any reductions in product selectivities, yields as well as the syngas product ratio. Fig. 10 shows the effect of excess CO 2 on carbon deposition. As the CO 2 : CH 4 ratio increased from 1:1 to 3:1, the carbon deposition, in grams per mole of methane, is decreased. The excess CO 2 provides higher reaction rates of Boudouard reaction or carbon oxidation reaction, in accordance to equation 14, with an increasing in CO% yield, as in full agreement with the experimental results.

Effect of Flow Rates on Methane Dry Reforming

In accordance to the results of previous section, the flow rates of the selected CO 2 /CH 4 of ratio 2: Water formation is likely independent on the effect of total flow rates of the CO 2 /CH 4 of ratio 2:1, as shown in Fig. 12. However, as the flow rate is decreasing, the CO% yield is significantly increased from 28% to 79%, revealing the positive effect of low flow rates on increasing the methane conversions, hydrogen and carbon monoxide yields. This maybe attributed to higher residence times. Consequently, this effect gives the opportunity for higher reaction rates of Boudouard reaction , shown in equation 14, for lower carbon deposition per mole methane. The result is illustrated in Fig. 13 Fig. 12, also shows the amount of stored energy in forms of H 2 and CO in KJ mol -CH 4 that can be estimated using the differences in the amount of heat released from the combusted methane of (-802 KJ mol -CH 4 ) and the amount of heat that can be released from the produced H 2 & CO during methane conversions. It can be noted that in case of higher flow rates of 50 and 30 ml/min, there is no energy storage as most of methane is converted to H 2 O, whereas at methane flow rate of 15ml/min the thermal storage energy in forms of 𝐻 2 and 𝐶𝑂 of approximately 156𝐾𝐽/𝑚𝑜𝑙 𝐶𝐻 4 with a storage efficiency of 63.1%.

Effect of Catalyst/ Molten Salt Ratio on Methane Dry Reforming

Fig. 14 shows the methane conversion and H 2 : CO production ratio, at constant reaction temperature of 800 o C and constant flow rates of both CH 4 and CO 2 of ratio of 1:1 at 50 mL/min, the amount of catalyst (10% Ni-Al2O 3 ) was changed with respect to molten salts (Cat./MS = 0.25, 0.5, 0.75, 1.0 & 1.25). The methane conversion was found increasing as the Cat./molten salts ratio is increased. It can be noted that the stoichiometric H 2 : CO production ratio of unity can be achieved at Cat./MS ratio between 1-1.25.

The curves of Fig. 14 has shown nearly the same trends of reported results of T. Kodama, T. Koyanagi, 2001, of their experimental data of reformed methane with CO 2 in (25g) alkali-carbonates Na 2 CO 3 , K 2 CO 3 (weight ratio = 1:1) at 1223K for a flow rate of the CH 4 / CO 2 feed was 200 ml/min.

Conclusion

Conceptual idea of DCBR was proposed to promote solar thermal energy storage, integrated with methane dry reforming, with a higher energy conversional capacity, higher thermal efficiency and greater simplicity of construction. The experimental results show the increase of CO 2 /CH 4 ratio in terms of higher methane conversion and CO yield, whereas the H 2 : CO production ratio was significantly decreasing, attributed to increase in water formation due to RWGS reaction. While, the carbon deposition is decreasing as per the theoretical results. The estimation of thermal energy stored chemically revealed a capacity of the storage efficiency of 63.1% at low temperatures of 600 -800 o C. However, this figure shall be increased at higher reaction temperatures and lower flow rates, as the RWGS reaction would be decreased.

Fig. 1 .

 1 Fig. 1. Experimental apparatus for CO 2 reforming of methane in a molten salt DCBR

Fig. 2 .

 2 Fig. 2. (a) Solidus Temperatures (b) Liquidus Temperatures, of mixed alkali-metal carbonate salts at different wt.% compositions of Li 2 CO 3 , Na 2 CO 3 and K 2 CO 3 2.3. Selection of a Catalyst and Preparation Some noble metal such as Rh, Ru, and Ir are very active for methane reforming. However, in commercial and industrial scale, it is not preferable as such expensive catalysts, especially, for methane dry reforming, would be technically and economically very difficult to reuse and recycle, in comparison with a conventional fixed bed reactor. The commonly cost effective catalysts used are Ni, Fe, Cu or W metal catalysts. (T. Kodama. 2001)[8]. Kodama has examined Ni, Fe, Cu or W metals, supported on Al 2 O 3 for activity and selectivity at 1223K. The most active and selective catalyst was the Ni -Al 2 O 3 catalyst for methane dry reforming in a molten carbonate salt bath for use in STC Processes. In this study, three types of Ni-Loading (10%, 15% & 20% wt.%) supported by α -Al 2 O 3 catalysts, were analyzed. The coke amount on the catalyst was examined by means of the mole balanced equations as would be explained in next section. The supported nickel catalyst on α -Al 2 O 3 was prepared by impregnation using Nickel (II) nitrate solution.

  5418 ˚A)) with graphite monochromator put on diffraction beam. The scanning diffraction pictures were carried out in the 2θrange of 20 o -80 o with 0.2 o step per 3s time of accumulation in a point. After the calcination treatment, dispersed Ni particles are presented in the oxide forms, Fig.3. The Ni% loading and calcination treatment does

Fig. 3 .

 3 Fig. 3. XRD Patterns of Ni% (10%, 15% & 20 wt. %) Loading Catalysts supported on Al 2 O 3

Fig. 4 .

 4 Fig. 4. TEM images of the Nickel metal loading catalysts before the reactions (a) 10% Ni-Al 2 O 3 (b) 15% Ni-Al 2 O 3 (c) 20% Ni-Al 2 O 3

Fig. 5 .Fig. 6 .Fig. 7 .Fig. 8 .

 5678 Fig.5. Effect of Ni% loading on methane dry reforming with 𝐂𝐎 𝟐 at reaction temperature of 𝟖𝟎𝟎 𝐨 𝐂, and 𝐂𝐇 𝟒 and 𝐂𝐎 𝟐 flow of ratio of 1:1 at 50 mL/min, during 4 hrs reaction time.

  1 was changed to (CH 4 flow rate of 15, 30 & 50mL/min) at constant reaction temperature of 800 o C. The Ar flow rate was kept constant at 30ml/min, and the catalyst used was 15% Ni -Al 2 O 3 . The methane conversion and hydrogen yield are decreasing as the total flow rate increases, as shown in Fig.11. The methane conversion decreased from 87% to 57% whereas hydrogen yield decreased from 40 to 9%.

Fig. 10 .Fig. 9 .

 109 Fig.10. Carbon deposition in g/mole-methane for various 𝐂𝐎 𝟐 /𝐂𝐇 𝟒 ratios, at constant reaction temperature of 𝟖𝟎𝟎 𝐨 𝐂 with constant 𝐂𝐇 𝟒 flow rate of 20 ml/min and constant total inlet flow rate of 100 ml/min Fig.9. Conversion (𝐂𝐇 𝟒 )%, Yield (𝐇 𝟐 )%, Yield (𝐂𝐎)%, and Yield (𝐇 𝟐 𝐎)% for various 𝐂𝐎 𝟐 /𝐂𝐇 𝟒 ratios, at constant reaction temperature of 𝟖𝟎𝟎 𝐨 𝐂 with constant 𝐂𝐇 𝟒 flow rate of 20 ml/min and constant total inlet flow rate of 100 ml/min

Fig. 12 .Fig. 14 .Fig. 11 .Fig. 13 .

 12141113 Fig.12. Conversion (𝐂𝐇 𝟒 )%, Yield (𝐇 𝟐 )%, Yield (𝐂𝐎)%, and Yield (𝐇 𝟐 𝐎)% and the amount of stored Energy (𝐊𝐉/𝐦𝐨𝐥 𝐂𝐇 𝟒 ) with the effect of total flow rate (methane flow rate) of 𝐂𝐎 𝟐 /𝐂𝐇 𝟒 ratio of 2:1, at const. reaction temperature of 𝟖𝟎𝟎 𝐨 𝐂 with constant 𝐀𝐫 flow rate of 30 ml/min -15% Ni-Al 2 O 3 catalyst

Table 1 . Crystallite sizes estimation of Ni% (10%, 15% & 20wt%) loading catalysts on Al 2 O 3

 1

  Ac denotes the total concentrations of the outlet flow of all species containing carbon element except Carbon black itself, B o denotes species containing oxygen element except H 2 O and C H denotes species containing Hydrogen element except H 2 O, as follows;

4 + CO 2 → αCH 4 + βCO 2 + γCO + δH 2 + εC 2 H 2 + ϵC 2 H 4 + θC 2 H 6 + ϑH 2 O + μO 2 + πC (2) Where α, β … π are the stoichiometric coefficients For methane reforming reaction with CO 2 , there are 10 species CH 4 , CO 2 , CO, H 2 , C 2 H 2 , C 2 H 4 , C2H6, H2O, O2, C and 3 elements (C, H, and O). If

Table 2 Table 2 . Values of a, b, n and m for different CH 4 :CO 2 Ratio

 22

Acknowledgements

Financial supports received in form of fellowship program from MASDAR Institute of Technology, Abu-Dhabi, which is gratefully appreciated.


Christophe Lecoutre
email: lecoutre@cril.fr

Sébastien

Sebastien Tabary
email: tabary@cril.fr

Abscon 112 Toward more Robustness

come

From Local to Global Variable Symmetries

In [START_REF] Lecoutre | Des symétries locales de variables aux symétries globales[END_REF], we have proposed to automatically detect variable symmetries of CSP instances by computing for each constraint scope a partition exhibiting locally symmetrical variables. From this local information that can be obtained in polynomial time, we can build a so-called lsv-graph whose automorphisms correspond to (global) variable symmetries. Interestingly enough, our approach allows us to disregard the representation (extension, intension, global) of constraints. Besides, the size of the lsv-graph is linear wrt the number of constraints (and their arity). To break symmetries from the generators returned by a graph automorphism algorithm, a classical approach is to post lexicographic ordering constraints defined on two vectors of variables. We have proposed a new variant of an algorithm enforcing GAC (generalized arc consistency) on such constraints which is able to deal with shared variables. This algorithm is quite simple to implement and well-adapted to general-purpose constraint solvers. Our experimental results show the robustness of the overall approach with different search heuristics: on a large number of series, more instances can be solved while the cpu time required for symmetry identification is observed as negligible. These results confirm that automatically breaking symmetries constitutes a significant breakthrough for black-box CSP solvers.

In order to show the practical interest of this approach, we have then conducted an extensive experimentation on a cluster of Xeon 3.0GHz with 1GiB of RAM under Linux. Here, performance is measured in terms of cpu time (in seconds) and number of visited nodes. We have integrated to the classical MAC algorithm, that is to say the algorithm that maintains (generalized) arc consistency at each node of the search tree, several variants of the symmetry breaking approach described in [START_REF] Lecoutre | Des symétries locales de variables aux symétries globales[END_REF]. For this experimentation, no restarts and no nogood recording were activated.

To identify variable symmetries, we have used Saucy. For each generator of the symmetry group returned by Saucy, we have considered four distinct symmetry breaking procedures. For the first one, denoted by M AC Le , a binary constraint of difference Le (constraint of the form x ≤ y) that involves the two first variables of the first cycle of the generator is posted. For the second one, denoted by M AC Lex , a lexicographic ordering constraint Lex (involving all variables of all cycles of the generator) is posted. Clearly, a Lex constraint is stronger than the corresponding Le constraint: its filtering capability is greater. Notice that when the two first variables of the first cycle of the generator are included in the scope of a (non-global) constraint c of the network, one can merge c with a binary constraint Le. In practice, if c is defined in intension, its associated predicate is modified whereas if c is defined in extension, the set of tuples disallowing the constraint Le are removed from the table associated with c. When such a merging method is applied, one obtains two additional procedures, denoted by M AC * Le and M AC * Lex .

Here, we only provide some results (see Table 1) obtained for the hardest instances (which involve 680 variables and a greatest domain size of about 50 values) built from the real-world Radio Link Frequency Assignment Problem (RLFAP). Clearly, the symmetry breaking methods allow us to be far more efficient than the classical MAC algorithm. In practice, M AC * Lex has been observed as the best method and has been used for the CSP competition.

Exploiting Cliques

Some instances contain hidden structures such as backbones, (strong) backdoors and unsatisfiable cores. Cliques also belong to this category. A clique is a graph such that there exists an edge between any two vertices. Interestingly, sometimes, we observe that for any pair (x, y) of variables of a sub-network P ′ of P whose constraint graph is a clique, the relation associated with the constraint involving x and y is irreflexive. Otherwise stated, we know that ∀{x, y} ⊂ vars(P ′ ), x = y. We can then infer an additional global constraint allDif f erent that can be useful to better prune the search space. However, in some constraint solvers, the filtering procedure (propagator) attached to allDif f erent achieves a local consistency weaker than generalized arc consistency. But, even in this case, inferring allDif f erent global constraints can be quite effective provided that the following (trivial) proposition is exploited.

Proposition 1. Let c : allDif f erent(x 1 , . . . , x r ) be a constraint. If we have | ∪ r i=1 dom(x i )| < r, then c is disentailed (i.e.

the set of supports of c is empty).

This approach is quite simple, and to the best of our knowledge, employed by some other solvers engaged in the 2008 competition. It suffices to detect cliques in a greedy manner, determine if irreflexivity is guaranteed between each pair of variables, and post a constraint allDif f erent that at least exploits Proposition 1. Interestingly, it is not so rare to find cliques in non-random problems. As an illustration, the instance blackHole-4-4-e-0 (see its constraint graph in Figure 1) contains a 16-clique that enables us to infer a global constraint allDif f erent. As one can show that this additional constraint is disentailed by using Proposition 1, the instance is directly proved to be unsatisfiable.

Simple Tabular Reduction

Table constraints play an important role within constraint programming. Recently, many schemes or algorithms have been proposed to propagate table constraints or/and to compress their representation. In [START_REF] Lecoutre | Optimization of simple tabular reduction for table constraints[END_REF], we have shown that simple tabular reduction (STR), a technique proposed by J. Ullmann [START_REF] Ullmann | Partition search for non-binary constraint satisfaction[END_REF] to dynamically maintain the tables of supports, is very often the most efficient practical approach to enforce generalized arc consistency within MAC. We have also described an optimization of STR which allows limiting the number of operations related to validity checking or search of supports. Interestingly enough, this optimization makes STR potentially r times faster where r is the arity of the constraint(s). The results of an extensive experimentation that we have conducted with respect to random and structured instances indicate that the optimized algorithm we propose is usually around twice as fast as the original STR and can be up to one order of magnitude faster than previous state-of-the-art algorithms on some series of instances.

In order to show the practical interest of simple tabular reduction, and in particular the optimization we propose, we have then experimented using a cluster of Xeon 3.0GHz with 1GiB of RAM under Linux, employing MAC with dom/ddeg and lexico as variable1 and value ordering heuristics, respectively. We have compared classical schemes to enforce GAC on (positive) table constraints with STR. More precisely, we have implemented the three schemes GACv, GACa and GACva described in [START_REF] Lecoutre | Generalized arc consistency for positive table constraints[END_REF]. We do believe that GACva is a representative state-ofthe-art algorithm for table constraints. Our own experience confirms the results reported in [START_REF] Gent | Data structures for generalised arc consistency for extensional constraints[END_REF]: GACva and the trie approach are quite robust and close in terms of performance.

Here, we only provide some results obtained for some series of Crossword puzzles. For each grid, there is a variable per white square which can be assigned any of the 26 letters of the Latin alphabet, and a constraint for any sequence of white squares which corresponds to a word that we must put in the grid. Such constraints are defined by a table which contains all words of the right length. The series prefixed by cw-m1c are defined from blank grids and only contain positive table constraints (contrary to model m1 in [START_REF] Beacham | Constraint programming lessons learned from crossword puzzles[END_REF] where no two identical words can be put in the grid, which is then naturally expressed in intension). The arity of the constraints is given by the size of the grids: for example, cw-m1c-lex-vg5-6 involves table constraints of arity 5 and 6 (the grid being 5 by 6).

The results that we have obtained (see Table 2) with respect to 4 dictionaries (lex, words, uk, ogd) of different length show the good performance of STR for such series. GACstr is the original algorithm, GACstr2 is the optimized version and GACstr2+ is GACstr2 made incremental. On the most difficult instances, GACstr2+ is about two times faster than GACstr and one order of magnitude faster than GACva. Note that we do not provide mean results for these series because many instances cannot be solved within 1, 200 seconds.

What about Max-CSP?

In order to participate to the part of the competition dedicated to Max-CSP, we have implemented in Abscon a variant of the PFC-MRDAC algorithm [START_REF] Larrosa | Maintaining reversible DAC for Max-CSP[END_REF]. This variant lies between PFC-MRDAC and PFC-MPRDAC [START_REF] Larrosa | Partition-Based lower bound for Max-CSP[END_REF].

For preprocessing, we have used a tabu search algorithm in order to obtain an initial lower bound of good quality. For (complete) search, we have used our PFC-MRDAC variant. We have integrated the pruning approach presented in [START_REF] Bennaceur | A decomposition technique for solving Max-CSP[END_REF].

Classical GAC schemes

Simple Tabular Reduction

GACv

GACa GACva GACstr GACstr2 GACstr2+

Crossword puzzles with dictionary lex (24, 974 words) cw-m1c-lex-vg5-6 cpu > As a consequence, a requirement was that the value ordering heuristic always selects the value with the lowest aic (arc-inconsistency count). Two variable ordering heuristics were tested: dom/wdeg [START_REF] Boussemart | Boosting systematic search by weighting constraints[END_REF] and dom * gap/ddeg that involves the aic gap of the variables [START_REF] Bennaceur | A decomposition technique for solving Max-CSP[END_REF]. More precisely, the ratio dom/ddeg is multiplied by the aic gap in order to favour variables for which there is a large gap between the best value and the following one.

Unfortunately, we omitted to remove a trace used for debugging. Consequently, the solvers have been considerably slowed down.

Some Deficiencies

Abscon 112 has suffered from two main deficiencies. First, in the category of global constraints, the solver was not ready altogether. Indeed, the constraint cumulative was not implemented and the filtering procedure for the constraint element not optimized. Second, as mentioned above, for Max-CSP, a trace output by the solver has considerably slowed down the resolution.

Fig. 1 .

 1 Fig.1. The constraint graph of the instance blackHole-4-4-e-0 contains a 16-clique. A constraint allDif f erent generated from this clique can be shown to be disentailed.

Table 1 .

 1 Cost of running MAC and its symmetry breaking variants on hard RLFAP instances (38 generators). The variable ordering heuristic is dom/wdeg.

			M AC M ACLe M ACLex M AC * Le	M AC * Lex
	scen11-f12	cpu nodes	1.88 390	2.0 614	2.05 721	1.71 4, 140	1.82 4, 140
	scen11-f11	cpu nodes	1.77 390	1.97 614	1.95 721	1.82 4, 216	1.83 4, 216
	scen11-f10	cpu nodes	1.77 468	1.82 327	2.08 722	1.81 109	1.9 77
	scen11-f9	cpu nodes	2.15 1, 064	1.96 576	2.23 922	1.84 109	1.97 90
	scen11-f8	cpu nodes	2.1 1, 354	2.09 558	2.28 997	2.02 112	2.0 115
	scen11-f7	cpu nodes	4.83 8, 369	2.28 955	2.37 1, 247	1.91 121	2.05 135
	scen11-f6	cpu nodes 17, 839 8.29	2.14 571	2.37 1, 333	2.1 172	2.08 157
	scen11-f5	cpu nodes 85, 104 32.0	2.2 988	3.13 3, 465	2.19 253	2.13 226
	scen11-f4	cpu nodes	112 345K	2.66 1, 983	3.88 5, 007	2.36 593	2.53 903
	scen11-f3	cpu nodes 1, 300K 403	3.41 3, 926	7.98 17, 259	2.55 946	2.45 696
	scen11-f2	cpu time-out nodes -	4.32 6, 014	16.4 40, 615	2.95 1, 700	2.92 1, 591
	scen11-f1	cpu time-out nodes -	7.56 14, 997	19.7 47, 318	3.49 3, 199	3.4 2, 609

Table 2 .

 2 Representative results obtained on series of Crossword puzzles using dictionaries of different length. Cpu time is given in seconds and mem(ory) in MiB. The number of nodes (#nodes) explored by MAC is given below the name of each instance.

		1, 200	38.8	54.2	14.3	12.4	10.7
	#nodes=26, 679	mem	2, 889K 2, 928K 2, 932K 2, 935K 2, 968K
	cw-m1c-lex-vg5-7 cpu > 1, 200	357	875	134	114	96.3
	#nodes=171K	mem	4, 134K 4, 173K 8, 005K 8, 055K 8, 059K
	cw-m1c-lex-vg6-6 cpu > 1, 200	2.98	4.29	1.28	1.05	0.91
	#nodes=1, 602	mem	4, 422K 4, 344K 4, 226K 4, 203K 4, 296K
	cw-m1c-lex-vg6-7 cpu > 1, 200	436	1, 174	176	143	118
	#nodes=152K	mem	5, 887K 5, 692K 9, 458K 9, 437K 9, 555K
	Crossword puzzles with dictionary words (45, 371 words)
	cw-m1c-words-vg5-5 cpu > 1, 200	0.04	0.05	0.05	0.05	0.04
	#nodes=38	mem	4, 969K 4, 987K 4, 823K 4, 791K 4, 809K
	cw-m1c-words-vg5-6 cpu > 1, 200	1.19	1.46	0.48	0.37	0.33
	#nodes=718	mem	6, 508K 6, 526K 6, 348K 6, 273K 6, 348K
	cw-m1c-words-vg5-7 cpu > 1, 200	18.6	36.0	6.61	5.21	4.03
	#nodes=6, 957	mem	8, 470K 8, 489K 8, 276K 8, 145K 8, 237K
	cw-m1c-words-vg5-8 cpu > 1, 200	866 > 1, 200	273	229	187
	#nodes=256K	mem	4, 604K		10M	10M	10M
	Crossword puzzles with dictionary uk (225, 349 words)
	cw-m1c-uk-vg5-5 cpu > 1, 200	0.05	0.05	0.1	0.07	0.07
	#nodes=28	mem	12M	12M	12M	12M	12M
	cw-m1c-uk-vg5-6 cpu > 1, 200	0.55	0.5	0.21	0.17	0.17
	#nodes=145	mem	17M	17M	16M	16M	16M
	cw-m1c-uk-vg5-7 cpu > 1, 200	2.97	5.18	0.51	0.37	0.34
	#nodes=408	mem	22M	22M	22M	22M	22M
	cw-m1c-uk-vg5-8 cpu > 1, 200	82.5	71.9	7.08	5.71	4.78
	#nodes=8, 148	mem	12M	12M	11M	11M	11M
	Crossword puzzles with dictionary ogd (435, 705 words)
	cw-m1c-ogd-vg6-6 cpu > 1, 200	0.37	0.31	0.23	0.17	0.15
	#nodes=98	mem	46M	47M	46M	46M	48M
	cw-m1c-ogd-vg6-7 cpu > 1, 200	95.3	56.1	12.0	8.01	6.81
	#nodes=9, 522	mem	11M	11M	11M	11M	11M
	cw-m1c-ogd-vg6-8 cpu > 1, 200	53.0	6.44	2.91	2.0	1.72
	#nodes=2, 806	mem	24M	23M	22M	22M	24M
	cw-m1c-ogd-vg6-9 cpu > 1, 200	727	214	35.1	25.1	19.1
	#nodes=23, 283	mem	42M	41M	39M	37M	40M

In our implementation, using dom/wdeg does not guarantee exploring the same search tree with classical and STR schemes.

Acknowledgements

This work has been supported by the CNRS and by the "IUT de Lens".


Daniel Le Berre
email: leberre@cril.univ-artois.fr

Anne Parrain
email: parrain@cril.univ-artois.fr

On SAT Technologies for dependency management and beyond

SAT solvers technology is now mature enough to be part of the engineer toolbox side by side with Mixed Integer Programming and Constraint Programming tools. As of June 2008, two great pieces of software are using SAT technology to manage dependency like problems: the open source Linux distribution OpenSuse 11.0, released on June 19, 2008, integrates a custom SAT solver in their dependency manager Zypp. The new update manager of Eclipse 3.4, called Equinox p2, also uses SAT technology to resolve dependencies in their OSGi platform. The use of SAT technology in Software Product Lines has already been pointed out by several authors. We believe that the current interest for solving dependency management problems in SAT technologies opens quite interesting challenges to the SAT community. First, since those problems are met in software with interactive use, SAT engines need to solve them within seconds. Second, providing one solution is usually not sufficient: finding the best solution is usually what users want. Finally, fully supported open source or commercial SAT engines are needed for a broader adoption in the software engineering community.

Introduction

The success of SAT technology in Electronic Design Automation (EDA), in particular in the area of Bounded Model Checking [START_REF] Biere | Symbolic model checking without bdds[END_REF] has pushed forward the development of SAT solvers. They are now being used routinely as lightweight constraint programming solvers. The performance breakthrough due to the Chaff SAT solver [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF], and the design some years later of the minimalistic Minisat [START_REF] En | An extensible sat-solver[END_REF] allowed the availability of numerous very efficient SAT engines in various languages. One of the main advantage of SAT solvers against more traditional constraint programming solvers is its simple unified input format (Dimacs [START_REF] Johnson | Second DIMACS implementation challenge : cliques, coloring and satisfiability[END_REF]) that allows SAT solvers to be used just as black boxes, or as SAT components in a more software engineering vocabulary.

If many users of SAT solvers are currently coming from EDA, the use of SAT technology is currently growing in software engineering. Recent works in software design analysis clearly focus on efficient translation into SAT [START_REF] Torlak | Kodkod: A relational model finder[END_REF] and take advantages of new features developed in SAT solvers (e.g. Unsat cores [START_REF] Torlak | Finding minimal unsatisfiable cores of declarative specifications[END_REF]) to improve both user experience and scalability. In Software Product Lines, SAT solvers can be used to decide whether a product configuration is safe or not and how to implement the product configuration [START_REF] Batory | Feature models, grammars, and propositional formulas[END_REF][START_REF] Thaker | Safe composition of product lines[END_REF]. Related work includes the use of CSP and BDD approaches to tackle the same problems [START_REF] Benavides | A first step towards a framework for the automated analysis of feature models[END_REF][START_REF] Benavides | FAMA: Tooling a framework for the automated analysis of feature models[END_REF]. The EDOS project [START_REF] Mancinelli | Managing the complexity of large free and open source package-based software distributions[END_REF][START_REF]The edos project[END_REF] found in SAT technology a good mean to validate the package dependencies for Linux distributions, i.e to answer the question:"Are all the packages of that distribution installable?". In the same spirit, OPIUM [START_REF] Tucker | Opium: Optimal package install/uninstall manager[END_REF] is a dependency manager for the Linspire linux distribution based on pseudo boolean solvers, one of the numerous extensions to SAT.

As a consequence of such research work on dependency management, two great pieces of software are using SAT technology to manage dependency like problems: the open source Linux distribution OpenSuse 11.01 , released on June 19, 2008, integrates a custom SAT solver in their dependency manager ZYpp. The new update manager of Eclipse 3.4, called Equinox p2, also uses SAT technology to resolve dependencies in its OSGi platform 2 . Finally, another famous framework for Java users, Maven, decided recently3 to use SAT technologies to resolve their package dependencies.

Dependency decision problem

Dependencies between packages can be easily modeled using propositional logic. For instance, package A depends on package B and package C can be expressed by the logical formula A → B ∧ C which in turn can be expressed by the two clauses A → B and A → C (or ¬A ∨ B and ¬A ∨ C). If all the dependencies are requirements of a conjunctive form, even if incompatibilities between packages are expressed, the resulting SAT problem is made of Horn clauses, i.e. clauses containing at most one positive literal, thus is solvable in linear time [START_REF] Dowling | Linear-time algorithms for testing the satisfiability of propositional horn formulae[END_REF].

The dependency problem becomes interesting when a given feature can be provided by several artifacts: this is the case for instance of several versions of the same OSGi bundle 4 in Eclipse. Sometimes, the same feature is provided by different packages, depending on their origin: to install latex in a linux distribution, one can use for instance texlive-latex or tetex-latex. In that case, we would express such dependency by something like latex → texlive latex ∨ tetex latex which is no longer a Horn clause. Thus the dependency problem becomes NP-complete [START_REF] Cook | The complexity of theorem-proving procedures[END_REF].

However, SAT solvers can nowadays solve some instances of the SAT problem with as many as millions of variables and clauses while they were still unable to solve a custom crafted 117 variables only SAT instance during the SAT 2007 Solver competition 5 . So, while there is no warranty that a SAT solver can solve efficiently SAT instances resulting from the translation of a "real" problem into SAT, it is often the case that such solvers perform well on those instances. From our own experience, the dependency decision problem can be easily solved using modern SAT solvers.

From satisfaction to optimization

However, the dependency problem is often underconstrained, which means that there is usually a lot of possible solutions. And not all those solutions are usually equally good. For Linux distributions for instance, one could take into account the number of packages to install, or their size, etc in order to propose an installation with the minimum number of packages or an installation with the smallest footprint on the hard drive. Those criteria can be easily modeled in an optimization framework by an objective function to minimize. Such objective function is of the form n i=1 a i x i where a i is an integral coefficient 4 OSGi is the component based model component chosen by Eclipse for its plug-in architecture. See http://www.osgi.org/ for details. 5 http://www.satcompetition.org/2007/ and x i is a propositional variable where true is denoted by value 1 and false is denoted by value 0.

If one wants to minimize the number of installed packages, all a i will be 1 and all x i will correspond to the propositional variables encoding packages to install. If one wants to minimize the size of the installed packages, then the a i will encode the size of each packages in bytes for instance.

In the case of SPL, the objective function could encode to install as many features as possible, to look for the cheapest or the most expensive product, etc.

Adding such objective function to a set of clauses creates an instance of the Binate Covering problem [START_REF] Coudert | On solving covering problems[END_REF]. Such problem has already been studied in EDA for logic synthesis (to minimize the number of components needed to perform a given operation). From a complexity theory, that problem is NP-hard, which means that is is at least as hard as SAT.

The binate covering problem can be seen as a very specific case of an Integer Linear Program in which case efficient ILP frameworks exist (e.g. CPLEX). However, it is currently not clear if ILP solvers are the right approach to tackle those problems. Indeed, ILP restricted to boolean variables has been also a recent area of research in the SAT community, under the generic name "Pseudo Boolean problems", inherited from the very first work on that subject [START_REF] Barth | Linear 0-1 inequalities and extended clauses[END_REF][START_REF] Barth | A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization[END_REF]. A competition of Pseudo Boolean solvers has been organized to assess the efficiency of existing solutions [START_REF] Manquinho | The first evaluation of pseudo-boolean solvers (pb'05)[END_REF]. Among the current best ones, one can note the pure SAT approach of Minisat+ [START_REF] Eén | Translating pseudo-boolean constraints into sat[END_REF], the hybrid approach Pueblo [START_REF] Sheini | Pueblo: A Hybrid Pseudo-Boolean SAT Solver[END_REF] (used in the tool OPIUM) or the modern branch-and-bound Bsolo [START_REF] Manquinho | On using cutting planes in pseudo-boolean optimization[END_REF]. Those solvers have been compared to the Gnu Linear Programming toolkit, and in many cases performed better. No comparison with commercial ILP solvers has been done yet.

In Artificial Intelligence, the binate covering problem is sometimes presented as a so called "Weighted partial MAX-SAT problem": the clauses of the original binate covering problem are called hard clauses, i.e. they must be satisfied. The objective function is encoded by weighted unit clauses, whose weight is a i and whose literal is ¬x i . If the weight is the same for all the soft clauses, the problem is called "partial MAXSAT". Since 2006, there is an annual competition of MAXSAT solvers. The interest on MAXSAT solvers is currently growing so MAXSAT solvers will be yet another way to tackle the binate covering problem in the future.

SAT solvers are currently efficient enough to solve SAT instances mapping real useful problems. Regarding solvers for SAT extensions like Pseudo Boolean or MAXSAT, the picture is less clear. Furthermore, we have seen that the so-called binate covering problem can be solved in many-ways: the best solution is yet to be determined.

The evaluation of the solvers is currently done on the assumption that the solvers are used in batch mode, i.e. that they can take several minutes, if not hours, to answer. Indeed, it is often the case in the area of model checking that the engineer writes its model during the day and let the SAT solver to check it during the night. In the SAT competition for instance, the timeout used in the industrial category is set to 1200 seconds in the first stage, and 10000 seconds in the second stage. As a consequence, the use of SAT solvers in interactive tools such as Eclipse or Linux update managers, or a Feature Model Editor such as FeatureIDE or FAMA requires specifically tailored solvers (see e.g. custom SAT engines in EDOS (debian) or OpenSuse.

Finally, the notion of quality of the solution is also a hot topic in that case: it is unlikely that a solver can efficiently solve all those NP-hard problems within a second, so non optimal solutions need to be returned after that time. We enter here in the area of anytime algorithms, for which local search algorithms are usually pretty good [START_REF] Hoos | Stochastic Local Search: Foundations & Applications[END_REF].

When modeling matters

The expected results mentioned in the previous section were simple, and global. However, in real applications, the user preferences are usually manifold and expressed in a local manner. Take for instance the case of the use of SAT technology in Eclipse p2: one expected result of the objective function is to make sure that most recent versions are installed preferably to older ones. If there is only one package, this is not a problem. However, as soon as there is more than one package, we enter the area of multiobjective/criteria optimization.

Indeed, suppose that package A is available in three versions: A 1 , A 2 , A 3 . Suppose that package B is available in two versions: B 1 , B 2 . Suppose that package X depends on A and B. The best solution would be to pick the latest versions, B 2 and A 3 . However, they are incompatible. Is it better to take A 2 and B 2 or B 1 and A 3 ? There is maybe no way to answer that question. In that case, an automated solution to solve that dependency problem will answer one of them, without any assumption that can be made on the solution. If one can add a preference between A and B, then we can discriminate between the two solutions and favor the first solution for instance if B is more important than A or the second one if A is more important than B.

Artificial Intelligence and Operational Research have solutions to deal with such kind of problems. In the specific case of Eclipse p2, the preferences on the different plugin versions could be modeled for instance using the Qualitative Choice Logic [START_REF] Brewka | Qualitative choice logic[END_REF].

Research toys or real tools?

There are numerous SAT/Pseudo Boolean/MAXSAT solvers out there, in various languages, with various features. However, very few are really supported in the sense that there is no clear way to get help, enter bug reports, etc. And very few are really open source: many solvers have a license restricting their use for research purpose only. Most of them are not full featured in the sense that if they all allow to solve the SAT decision problem, very few support also proof logging, minimal unsat core, model enumeration, model counting, optimization support, support for multi-core processors, etc. In that sense, users of SAT technology must first define all the features they really need in order to choose the right solver (or the right solvers, since it might be just impossible to find a solver with all needed features). In that sense, SAT solvers are still research toys.

On the other hand, various products (from both academia and private companies) are now based on currently available SAT solvers. So the same solvers can be considered as real tools too.

The main current issue is certainly the input format used in the SAT community: the Dimacs format created for the Second Dimacs Challenge [START_REF] Johnson | Second DIMACS implementation challenge : cliques, coloring and satisfiability[END_REF]. It is a simple integer based input format very convenient for SAT solver developers. It's simplicity is one key element of the incredible evolution of SAT solvers: everybody can easily read or produce SAT instances using that format, in any language. As a consequence, SAT solvers became quickly "black-boxes" fed using Dimacs formatted SAT instances. It was thus easy to compare the behavior of several solvers on the same benchmarks, organize sat competitions, etc. However, it is not a nice input format for people willing to try SAT technology: one needs to design an abstraction layer between its problem and the Dimacs format or the SAT solver first. The audience of SAT technology growing, a more user friendly input format is now necessary.

Conclusion

We have seen that SAT technology receives currently a lot of attention in the software engineering community, especially in the area of dependency management, that is also a concern inherent to Software Product lines. We have seen that the basic decision problem related to dependency management is in practice easily solvable with current state-ofthe-art SAT solvers. However, dependency management in real software is likely to be better modelled as an optimization problem called binate covering problem for which numerous solutions exist. We currently do not know the best approach for solving binate covering instances encoding the dependency problem. Another issue with dependency management lies in the fact that the problem is likely to be under-constrained, i.e. it is likely that the problem admit several equivalent solutions for the solver. As a consequence, it will be very difficult to control the answers provided by the solver, and to offer some warranties about those solutions. It must be clear for users of such technology that the most important part of the work is to properly express their problem in terms of preferences among possible solutions, then to deduce from those preferences the objective function of their binate covering problem. Finally, the use of solvers in interactive tools is likely to change the solvers landscape since most of them are currently designed to be used in batch mode.

http://en.opensuse.org/OpenSUSE_11.0

http://wiki.eclipse.org/Equinox_P2_Resolution

http://jira.codehaus.org/browse/MARTIFACT-20

This work is supported in part by the European research project number 214898 Mancoosi (www.mancoosi.org).