Phasing genotypes from sequence data is an important step betweendata gathering and downstream analysis in population genetics,disease studies, and multiple other fields. This determination ofthe sequences of markers corresponding to the individualchromosomes can be done on data where the markers are in lowdensity across the chromosome, such as from single nucleotidepolymorphism (SNP) microarrays, or on data with a higher localdensity of markers like in next generation sequencing (NGS). Thesorted markers may then be used for many different analyses anddata processing such as linkage analysis, or inference of missinggenotypes in the process of imputation cnF2freq is a haplotype phasing program that uses an uncommonapproach allowing it to divide big groups of related individualsinto smaller ones. It sets an initial haplotype phase and theniteratively changes it using estimations from Hidden MarkovModels. If a marker is judged to have been placed in the wronghaplotype, a switch needs to be made so that it belongs to thecorrect phase. The objective of this project was to go fromallowing only one individual within a group to be switched in aniteration to allowing multiple switches that are dependent on eachother. The result of this project is a theoretical solution for allowingmultiple dependent switches in cnF2freq, and an implementedsolution using the max-SAT solver toulbar2.

Many problems that arise in the real world are difficult to solve partly because they present computational challenges. Many of these challenging problems are optimization problems. In the real world we are generally interested not just in solutions but in the cost or benefit of these solutions according to different metrics. Hence, finding optimal solutions is often highly desirable and sometimes even necessary. The most effective computational approach for solving such problems is to first model them in a mathematical or logical language, and then solve them by applying a suitable algorithm. This thesis is concerned with developing practical algorithms to solve optimization problems modeled in a particular logical language, MAXSAT. MAXSAT is a generalization of the famous Satisfiability (SAT) problem, that associates finite costs with falsifying various desired conditions where these conditions are expressed as propositional clauses. Optimization problems expressed in MAXSAT typically have two interacting components: the logical relationships between the variables expressed by the clauses, and the optimization component involving minimizing the falsified clauses. The interaction between these components greatly contributes to the difficulty of solving MAXSAT. The main contribution of the thesis is a new hybrid approach, MaxHS, for solving MAXSAT. Our hybrid approach attempts to decouple these two components so that each can be solved with a different technology. In particular, we develop a hybrid solver that exploits two sophisticated technologies with divergent strengths: SAT for solving the logical component, and Integer Programming (IP) solvers for solving the optimization component. MaxHS automatically and incrementally splits the MAXSAT problem into two parts that are given to the SAT and IP solvers, which work together in a complementary way to find a MAXSAT solution. The thesis investigates several improvements to the MaxHS approach and provides empirical analysis of its behaviour in practise. The result is a new solver, MaxHS, that is shown to be the most robust existing solver for MAXSAT.

Many problems that arise in the real world are difficult to solve partly because they present computational challenges. Many of these challenging problems are optimization problems. In the real world we are generally interested not just in solutions but in the cost or benefit of these solutions according to different metrics. Hence, finding optimal solutions is often highly desirable and sometimes even necessary. The most effective computational approach for solving such problems is to first model them in a mathematical or logical language, and then solve them by applying a suitable algorithm. This thesis is concerned with developing practical algorithms to solve optimization problems modeled in a particular logical language, MAXSAT. MAXSAT is a generalization of the famous Satisfiability (SAT) problem, that associates finite costs with falsifying various desired conditions where these conditions are expressed as propositional clauses. Optimization problems expressed in MAXSAT typically have two interacting components: the logical relationships between the variables expressed by the clauses, and the optimization component involving minimizing the falsified clauses. The interaction between these components greatly contributes to the difficulty of solving MAXSAT. The main contribution of the thesis is a new hybrid approach, MaxHS, for solving MAXSAT. Our hybrid approach attempts to decouple these two components so that each can be solved with a different technology. In particular, we develop a hybrid solver that exploits two sophisticated technologies with divergent strengths: SAT for solving the logical component, and Integer Programming (IP) solvers for solving the optimization component. MaxHS automatically and incrementally splits the MAXSAT problem into two parts that are given to the SAT and IP solvers, which work together in a complementary way to find a MAXSAT solution. The thesis investigates several improvements to the MaxHS approach and provides empirical analysis of its behaviour in practise. The result is a new solver, MaxHS, that is shown to be the most robust existing solver for MAXSAT.

Στην εργασία αυτή ασχοληθήκαμε με το πρόβλημα της Πιθανοτικής Ικανοποιησιμότητας. Παρουσιάσαμε ανάλυση της πολυπλοκότητας του προβλήματος και το επιλύσαμε με την βοήθεια του λογισμικού πακέτου CPLEX. Περιγράψαμε προσεγγιστικούς αλγόριθμους για το πρόβλημα της Μέγιστης Ικανοποιησιμότητας που χρησιμοποιείται στην διαδικασία της Column Generation. Τέλος, πριγράψαμε το αντίστροφο πρόβλημα των συχνών στοιχειοσυνόλων και την σχέση του με το πρόβλημα της Μέγιστης Ικανοποιησιμότητας. / This thesis is about the problem of probabilistic satisfiability. We describe its computational complexity, we solve the problem using CPLEX, we discribe some approximations on Maximum Satisfiability. Finally, we describe the connection between the problem of Probabilistic Satisfiability and the inverse frequent itemset mining.