 |
|
Projectos de Investigação Científica e de Desenvolvimento Tecnológico em Todos os Domínios Científicos
Concurso 2004 |
Resumo do Projecto |
| |
Imprimir esta página
Print this page
Voltar
Back
Referência do projecto
Project reference |
| |
| POSC/EIA/61852/2004 |
|
1. Identificação do projecto
1. Project description
|
Área científica principal
Main Area
|
|
Computer Engineering
|
Área científica Secundária
Secondary area
|
|
Mathematics
|
Título do projecto (em português)
Project title (in portuguese)
|
| SATPot: Algoritmos de satisfação, aplicações e extensões |
Título do projecto (em inglês)
Project title (in english)
|
| SATPot: SATisfiability algorithms, aPplicatiOns and exTensions |
| Palavra-chave 1 |
Keyword 1 |
| Satisfação Proposicional |
Boolean Satisfiability |
| Palavra-chave 2 |
Keyword 2 |
| Optimização Pseudo-Booleana |
Pseudo-Boolean Optimization |
| Palavra-chave 3 |
Keyword 3 |
| Fórmulas Booleanas Quantificadas |
Quantified Boolean Formulas |
| Palavra-chave 4 |
Keyword 4 |
| Contagem de Modelos |
Model Counting |
Objectivos sócio-económicos
Socio-economic objectives |
| Industry - General research |
2. Financiamento Atribuído
2. Funding
|
| 88.000,00 Euros |
|
3. Instituições participantes
3. Participating institutions
|
Instituição Proponente
Principal Contractor |
| Instituto de Engenharia de Sistemas e Computadores, Investigação e Desenvolvimento em Lisboa (INESC ID/INESC/IST/UTL)
|
Rua Alves Redol, 9
1000-029 Lisboa
|
|
Instituições Participantes
Participating Institutions |
(vazio)
(void) |
|
Unidade de Investigação
Principal Research Unit |
| Instituto de Engenharia de Sistemas e Computadores, Investigação e Desenvolvimento em Lisboa (INESC ID/INESC/IST/UTL) |
Rua Alves Redol, 9
1000-029 Lisboa |
|
Instituição de Acolhimento
Host Institution |
| Instituto de Engenharia de Sistemas e Computadores, Investigação e Desenvolvimento em Lisboa (INESC ID/INESC/IST/UTL) |
Rua Alves Redol, 9
1000-029 Lisboa |
|
4. Equipa de investigação
4. Research team
|
Lista de membros (10)
Members list (10) |
Nome
Name |
Função
Role |
Grau académico
Academic degree |
%tempo
%time |
| Maria Inês Camarate de Campos Lynce de Faria |
Inv. Responsável |
DOUTORAMENTO |
70 |
|
| João Paulo Marques Silva |
Investigador |
AGREGAÇÃO |
10 |
|
| Vasco Miguel Gomes Nunes Manquinho |
Investigador |
DOUTORAMENTO |
70 |
|
| Luis Manuel Tremoceiro Baptista |
Investigador |
MESTRADO |
50 |
|
| Elsa Cristina Batista Bento Carvalho |
Investigador |
LICENCIATURA |
50 |
|
| António José dos Reis Morgado |
Bolseiro |
MESTRADO |
100 |
|
| Paulo Jorge de Oliveira Cantante de Matos |
Bolseiro |
MESTRADO |
100 |
|
| José Faustino Fragoso Femenin dos Santos |
Bolseiro |
MESTRADO |
100 |
|
| David Miguel Never Pereira |
Bolseiro |
|
100 |
|
| João Benigno Delgado |
Bolseiro do projecto |
|
100 |
|
| |
|
Resumo (em português)
Abstract (in portuguese) |
| A Satisfação Booleana (SAT) é um problema de decisão referencial em teoria da complexidade, conhecido por ser NP-completo. Algumas das suas extensões também são conhecidas como referenciais em teoria da complexidade, um exemplo são as Fórmulas Booleanas Quantificadas (QBF) para problemas de decisão P-espaço completos.\nAo longo da última década a área dos algoritmos de SAT tem presenciado melhoramentos dramáticos. De curiosidade essencialmente académica no início da década de 90, os algoritmos de SAT evoluiram de tal modo que a sua utilização é generalizada num conjunto significativo de aplicações comerciais, destas a mais representativa sendo a verificação de modelos em sistemas de hardware, software e embebidos. Apesar da sua utilização generalizada em aplicações comerciais, os algoritmos de SAT têm continuado a evoluir ao longo dos anos. No entanto, a utilização industrial generalizada de algoritmos de SAT, e os desafios que esta utilização coloca, motivam que a investigação em SAT continue o desenvolvimento de algoritmos cada cada vez mais optimizados, capazes de resolver instâncias cada\nvez mais difíceis.\nAlém de SAT, um número de áreas relacionadas foram também sujeitas a melhoramentos dramáticos. Exemplos incluem algumas extensões conhecidas de SAT, nomeadamente Optimização Pseudo-Booleana (PBO), Contagem de Modelos em SAT (#SAT) e QBF.\nO projecto SATPot posiciona-se como um componente chave da estratégia da equipa de investigação para continuar trabalho de investigação de qualidade e aumentar a visibilidade internacional nas áreas de SAT, extensões e aplicações. Por outro lado, o projecto pretende representar um elemento agregador que inclui investigação em SAT, em extensões de SAT e em aplicações de SAT, todas baseadas num núcleo algorítmico comum.\nO projecto propõe também um conjunto de ideias novas para melhorar o estado da arte dos algoritmos de SAT, além de um conjunto de ideias para melhorar os algoritmos em áreas relacionadas, nomeadamente PBO, #SAT, e QBF. Como uma extensão natural, o projecto pretende também criar competências em MV-SAT e MathSAT. O trabalho proposto encontra-se dividido em duas componentes principais: o desenvolvmento de um novo núcleo para SAT, e o estudo e desenvolvimento de técnicas de domínio específico, para SAT, PBO, #SAT e QBF.\nAlém do desenvolvimento de novos algoritmos, com impacto directo em aplicações bem conhecidas, e.g. verificação de modelos em sistemas reactivos, o projecto SATPot também pretende a promoção da utilização de SAT e extensões de SAT em empresas Portuguesas. Para atingir este objectivo, um conjunto de aplicações, consideradas relevantes, serão estudadas e contactos com empresas representativas serão explorados. Estas aplicações incluem a detecção e correcção de erros em dados estatísticos, soluções para o problema da atribuição de frequências em comunicações móveis, técnicas de encaminhamento em fibra óptica, e a verificação de especificações de processos de negócio. Todas estas aplicações têm potencial estratégico, e podem ser naturalmente resolvidas com SAT ou com extensões de SAT. |
| |
Resumo (em inglês)
Abstract (in english) |
| Boolean Satisfiability (SAT) is a referential decision problem in complexity theory, well-known for being NP-complete. Some of its extensions are also well-known for being referential in complexity theory, e.g. Quantified Boolean Formulas (QBF) for P-Space complete decision problems.\nOver the last decade the area of SAT algorithms has been the subject of dramatic improvements. From a mostly academic curiosity in the early 90´s, SAT algorithms evolved to a stage where their use is widespread in a large number of commercial applications, the most significant being Model Checking of hardware, software and embedded systems. Despite their widespread utilization in industrial settings, SAT algorithms have continued to evolve over the years. Nevertheless, the widespread industrial use of SAT algorithms, and the challenges this unveils, further motivates SAT research to continue developing ever more optimized algorithms, capable of solving ever more challenging problem instances.\nBesides SAT, a number of related areas have also been the subject of dramatic improvements. Examples include well-known extensions of SAT, namely Pseudo-Boolean Optimization (PBO), Counting Models in SAT (#SAT) and Quantified Boolean Formulas (QBF).\nThe SATPot project is expected to be a key component of the research team strategy for continuing quality research work and further extending the international visibility in the areas of SAT, extensions and applications. Moreover, the SATPot project represents a container that includes research on SAT, on SAT extensions and on SAT applications, all based on a unified algorithmic core.\nThe SATPot project also proposes a number of new ideas for improving state of the art SAT solvers, as well as a number of ideas for improving algorithms in related areas, namely PBO, #SAT and QBF. As a natural extension, the SATPot project also aims creating competencies in MV-SAT and MathSAT. The proposed work is organized in two main components: the development of a new SAT core, to be used in SAT and in SAT extensions, and the study and development of domain-specific techniques, for SAT, PBO, #SAT and QBF.\nBesides the development of new algorithms, with key direct impact in well-known applications, e.g. model checking of reactive systems, the SATPot project also aims promoting the utilization of SAT and SAT extensions in Portuguese companies. For achieving this goal, a number of applications, considered relevant to the Portuguese economy, will be studied and contacts with representative companies will be pursued. These include detection and correction of errors in statistical data, solutions to the frequency assignment problem in wireless communications, techniques for routing in fiber optics, and the verification of business process specifications. All these applications have strategic potential in the Portuguese economy, and can be naturally addressed either with SAT or with SAT extensions. |
| quinta-feira, 2 de Setembro de 2010 |
|
| |
| |
|