The interest in SAT solving has increased mainly due to improvements in the solving algorithms, whichincreasingly have focused on using parallelism offered by multi-CPU computers. Partly orthogonally to these improvements, this work studies several novel approaches to parallel solving of SAT instances in a grid of widely distributed "virtual" computers instead of workstations or supercomputers.

The doctoral dissertation of Licentiate of Science (Technology) Hyvärinen ( right) examines the solving of hard structured problems using cloud computing, where cloud computing can significantly speed up problem solving and save energy. Cloud computing translating into  decentralising IT services so that tens, hundreds or thousands of distributed computers can be used simultaneously. 

Hyvärinen says that solving practical problems often requires going through large amounts of data efficiently and performing automatic inference based on the material. For instance, when the link between certain genes and the onset of a disease is studied, the material from which correlations should be found, can be extremely extensive. 

Cloud computing speeds up solving a problem because it is possible to use thousands of computers instead of just one. Instead of spending ten years looking for a solution, the computers may solve the problem in a matter of hours.

Decentralising computers will also saves energy. Computers produce a lot of heat and there is a major demand for computing capacity in large cities in the south. Due to the warm climate in these areas, cooling the heat produced by the computers consumes a lot of electricity. Hyvärinen says that now the speed of computer processors executing program commands, will no longer increase significantly. If  faster results are wanted in the future, computing should be performed in parallel by several or many computers.

However, parallel programming is difficult. The dissertation presents several analytical and experimental results that offer solutions to the problems related to parallel processes. These new methods can be used to solve several previously unsolved problems for the first time. In practice, certain algorithms have been developed so that they can more efficiently make use of several processors simultaneously, decreasing the computational time.

Hyvärinen uses a propositional logic to model structured problems. Due to its general nature, this logic enables the modelling of different types of problems from bioinformatics to artificial intelligence design.