PROVERBS -- PRobabilistic OVERconstrained Boolean Systems: reasoning tools and applications

Abstract

Solving computational problems on real world objects means to bring together strict models of the universe of discourse, with less than perfect and flexible information one may gather about the world. This means that the solution method must be able to cope both with hard and well-defined statements on the world with other information whose nature is soft. The capability to deal with such a situation may enable us to deal with computer devices placed at a real world, with its often changing, imprecise and uncertain flow of information.This project studies problems that combine real-world hard constraints with soft constraints involving preferences, uncertainties and flexible requirements. In this work, the hard constraints are represented by sets of Boolean formulas. The soft constraints may take the form of weights of preference associated to some of the Boolean formulas, with the goal of maximizing the total weight of the satisfied soft constraints. This is the \emph{maximum satisfiability (MaxSAT)} approach to the problem of hard and soft constraints. Another way to model soft constraints is to associate probabilities to some of the formulas, in which case a solution is a probability distribution over the models that meet the hard constraints, that also verifies the soft probability constraints. This is the \emph{probabilistic satisfiability (PSAT)} approach to hard and soft constraints.In many situations, both modelling techniques of hard and soft Boolean constraints lead to \emph{overconstrained} formulations, that is, a set of constraints for which no consistent interpretation is possible. Important applications modelled by overconstrained hard-soft problems are found in several areas, among which the following will be explored in this project: Security, protocol verification and planning, and computational linguistics.However, the nature of these constraints place us in the middle of the \emph{intractable} computational class known as NP-hard, for which no efficient general algorithm is know, but for which many simpler instances have been discovered in the recent years. We believe that a cross fertilization between these two approaches can lead to significant progress in dealing with hard-soft constraints. By combining the expertise of top-tier researchers in both approaches, this project aims at leading the technique and applications of the area to a different level.We plan to develop several algorithms to deal with MaxSAT and PSAT problems, including the solution of PSAT using MaxSAT. We then plan to apply those techniques to the solution of overconstrained problems. Programs will be made available as free and open-source software. Applications of these techniques and algorithms will cover the areas of information security, protocol verification and computational linguistics.This project is the Brazilian side of a collaboration between research groups based at two universities in Portugal and Brazil that aim at studying these methods and exploring approaches for the problem of dealing with probabilistic over constrained problems. (AU)