O presente trabalho tem como objetivo um estudo sobre perfil de consumidor e o problema de localização de lojas de diferentes canais de vendas do varejo, levando em consideração o perfil socioeconômico e perfil de compra dos consumidores. Uma análise de clusters possibilitou, com base nos dados de vendas por classes sócio-econômicas de lojas dos vários canais obtidos de um varejista, a segmentação de diferentes tipos de lojas e canais com potenciais de vendas diferenciados. Posteriormente, a pesquisa propõe uma modelagem para o problema de localização dos grupos de loja no varejo empregando programação linear inteira. O modelo visa à maximização do resultado operacional total que se obtém da política de localização de diferentes tipos de lojas e canais numa cidade ou região. O modelo é implementado para a cidade de Belo Horizonte (MG), utilizando-se os dados levantados de potenciais de vendas para os diferentes tipos de canais lojas e os dados da distribuição das populações dos bairros de BH, segmentados pelas várias classes sócioeconômicas. Uma análise de Sensibilidade apresenta os efeitos de diferentes formas de operacionalização da área de influência ou cobertura de uma loja sobre a política de localização das lojas, bem como sobre o resultado operacional. A análise sensibilizada mostrou também que o modelo buscou dentre os diferentes cenários alterados, a aproximação na indicação dos bairros a ser instalados as lojas, ao percentual de influência e ao potencial de vendas dos diferentes bairros por tipos de lojas. A segmentação das lojas em vários tipos e canais bem como a proposição de operacionalização da região de cobertura de uma loja contribuem com discussões importantes para a literatura. Por outro lado, a modelagem proposta pode apresentar subsídio para a tomada de decisão gerencial na expansão ou implantação de lojas de varejo numa determinada região. / The main objective of the present research aims to a study on consumer profile and the retail store location problem of different stores channels, taking into account the socioeconomic profile and the consumers purchase behavior. A clusters analysis, based on sales data for socio-economic classes from the various type of stores channels obtained from a retailer, targeted of different types of stores and channels different sales potential. Subsequently, the research proposes a model to the problem of location of groups of retail store employing integer linear programming. The model aims to maximize the total operational result that is obtained from the optimal location of different types of stores and channels in a city or region. It is implemented for the city of Belo Horizonte (MG), using data collected from the sales potential for the different types of stores channels and of distribution of the populations on each districts in BH, targeted by the various socio-economic classes. A sensitivity analysis shows the effects of various types of operation of the area of influence or coverage of a shop on the politics of location of the shops, as well as the operating result. The sensitive analysis also showed that the model sought among the changes of parameters over the scenarios, the proximity over the indication of districts to the store indication, the influence percentage and the sales potential over the different districts by store cluster. The segmentation of the stores throughout the various types and channels as well as the proposition of area coverage operation of a single store, contributes to important literature discussions. Moreover, the proposed model may subsidizes management of decision-making in expansion or establishment of retail stores in a given region.

High school timetabling problems consist in assigning meetings between classes and teachers, with the goal of minimizing the violation of specific soft requisites. This category of problems has been extensively studied since the 1950s, mostly via mixed-integer programming and metaheuristic techniques. However, the computation of optimal or near-optimal solutions using mixed-integer programs or metaheuristics is still a challenge for most practical problems. In this thesis, we investigate new mixed-integer programming formulations, column generation approaches and parallel metaheuristic based algorithms to compute lower bounds and solutions for high school timetabling problems. Extensive computational experiments conducted with real-world instances demonstrate that our best formulations are competitive with best-known formulations, while our parallel algorithms present superior performance than the state-of-the-art methods. / Problemas de horários escolares consistem em alocar encontros entre turmas e professores, com objetivo de minimizar violações a requisitos qualitativos específicos. Esta categoria de problemas tem sido largamente estudada desde 1950, particularmente via técnicas de programação linear inteira mista e metaheurísticas. Entretanto, a computação de soluções ótimas ou quase ótimas usando programas inteiro-mistos ou metaheurísticas ainda é um desafio na maioria dos problemas práticos. Nesta tese, nós investigamos novas formulações inteiro-mistas, decomposições por geração de colunas e algoritmos baseados em metaheurísticas paralelas para computar limitantes inferiores e soluções para problemas de horários escolares. Extensivos experimentos computacionais conduzidos com instâncias reais demonstram que nossas melhores formulações são competitivas com as melhores formulações existentes, enquanto nossos algoritmos paralelos são superiores em performance computacional quando comparados com métodos que são estado-da-arte.

This paper aims to present the thesis developed in the Doctoral Programin Computer Science and Computational Mathematics of the ICMC/USP. The thesis theme seeks to advance the state of the art by solving the problems of scalability and representation present in mission planning algorithms for Unmanned Aerial Vehicle (UAV). Techniques based on mathematical programming and evolutionary computation are proposed. Articles have been published, submitted or they are in final stages of preparation.These studies report the most significant advances in the representation and scalability of this problem. Mission planners worked on the thesis deal with stochastic problems in non-convex environments,where collision risks or failures in mission planning are treated and limited to a tolerated value. The advances in the representation allowed to solve violations in the risks present in the original literature modeling, besides making the models more realistic when incorporating aspects such as effects of the air resistance. Efficient mathematical modeling techniques allowed to advance from a Mixed Integer Nonlinear Programming (MINLP) model, originally proposed in the literature, to a Mixed Integer Linear Programming (MILP) problem. Modeling as a MILP led to problem solving more efficiently through the branch-and-algorithm. The proposed new representations resulted in improvements from scalability, solving more complex problems within a shorter computational time. In addition, advances in scalability are even more effective when techniques combining mathematical programming and metaheuristics have been applied to the problem. / O presente documento tem por objetivo apresentar a tese desenvolvida no Programade Doutorado em Ciência da Computação e Matemática Computacional do ICMC/USP. O tema da tese busca avançar o estado da arte ao resolver os problemas de escalabilidade e representação presentes em algoritmos de planejamento para missões com Veículos Aéreos Não Tripulados (VANTs). Técnicas baseadas em programação matemática e computação evolutiva são propostas. Artigos foram publicados, submetidos ou se encontram em fase final de elaboração. Esses trabalhos reportamos avanços mais significativos obtidos na representação e escalabilidade deste problema.Os planejadores de missão trabalhados na tese lidam com problemas estocásticos em ambientes não convexos, onde os riscos de colisão ou falhas no planejamento da missão são tratados e limitados a um valor tolerado. Os avanços na representação permitiram solucionar violações nos riscos presentes na modelagem original, além de tornar os modelos mais realistas ao incorporar aspectos como efeitos da resistência do ar. Para isso, técnicas eficientes de modelagem matemática permitiram avançar de um modelo de Programação Não-Linear Inteira Mista(PNLIM), originalmente proposto na literatura, para um problema de Programação Linear Inteira Mista (PLIM). A modelagem como um PLIM levou à resolução do problema de forma mais eficiente através do algoritmo branch-and-cut. As novas representações propostas resultaram em melhorias na escalabilidade, solucionando problemas mais complexos em um tempo computacional menor.Além disso,os avanços em escalabilidade mostraram-se mais efetivos quando técnicas combinando programação matemática e metaheurísticas foram aplicadas ao problema.

Orientador: Fábio Bertequini Leão / Resumo: Este trabalho apresenta modelos de programação não linear e linear inteira binária como novos métodos para resolver o problema de diagnóstico de faltas em sistemas de transmissão de energia elétrica. Os modelos de otimização são desenvolvidos com base no conjunto de coberturas mínimas e possui como restrições as equações que descrevem a lógica e a filosofia de proteção empregadas por empresas de energia elétrica. As equações de restrições modelam a associação dos alarmes dos relés de proteção informados pelo sistema de supervisão e aquisição de dados (SCADA) com os estados esperados das funções dos relés de proteção. Os modelos de programação matemática realizam o diagnóstico de falta em uma única etapa, identificando a seção em falta através da análise dos estados dos disjuntores e das funções de proteção associadas a cada equipamento do sistema elétrico. O modelo proposto é um problema muito complexo de programação não linear inteira binária, portanto é reformulado como outro problema, em que algumas expressões são linearizadas, o que resulta em um modelo matemático de programação linear inteiro binário. A solução ótima obtida pelo modelo proposto é encontrada utilizando solvers comerciais de programação matemática. Os resultados obtidos mostram eficiência e robustez do modelo matemático. Na literatura, o problema de diagnóstico de falta é resolvido principalmente por técnicas heurísticas, portanto, o método proposto é inovador. / Doutor

Atualmente, os hospitais se veem obrigados a melhorar sua produtividade. Os centros cirúrgicos, além de ser um dos setores com maiores custos, também é o que mais gera receita dentro de um hospital, dessa forma torna-se extremamente importante o gerenciamento eficiente desse setor. Os métodos de otimização para programação de cirurgias podem ser usados como ferramentas para reduzir filas e ociosidade nos centros cirúrgicos, aumentando sua produtividade. O Problema de Programação de Cirurgias Eletivas com Múltiplos Recursos e Múltiplas Etapas consiste em alocar os recursos às etapas do processo cirúrgico dos pacientes, considerando as diferentes necessidades e rotas de cada paciente e, então, programar essas etapas no tempo respeitando a disponibilidade dos recursos e a sequência das etapas do processo cirúrgico dos pacientes. Esse problema é classificado na literatura como NP-hard e pode ser descrito como um Job Shop Flexível com blocking e função objetivo de minimização do número de pacientes não atendidos e do instante de término da última etapa, o makespan. O Objetivo desse trabalho é propor um modelo matemático e uma heurística construtiva para a resolução desse problema. O modelo matemático Multi-Mode Blocking Job Shop (MMBJS) apresentado em Pham e Klikert (2008) é explorado e algumas melhorias são apontadas neste trabalho. Um modelo matemático de Programação Linear Inteira Mista alternativo é proposto, a fim de reduzir o esforço computacional, ajustar o cálculo do makespan e sugerir uma estratégia de priorização de pacientes. Testes computacionais foram realizados, afim de comparar o modelo MMJBS e o modelo proposto. Para instâncias em que todos os pacientes são atendidos, as soluções encontradas pelo CPLEX para ambos modelos são iguais, porém o tempo computacional necessário para encontrar uma solução ótima é em média 45% menor no modelo proposto. Também foram realizados testes computacionais com objetivo de observar o comportamento do modelo com diferentes configurações de recursos. Para instâncias com 15 pacientes, os testes apontam que o tempo computacional para encontrar a solução ótima é superior a 2h de processamento. Dessa forma, uma heurística construtiva é proposta, com objetivo de gerar soluções factíveis com pouco esforço computacional. A heurística proposta aloca cada etapa do tratamento de cada paciente aos recursos necessários, respeitando as janelas de disponibilidade dos recursos e buscando reduzir a folga no sistema. Um exemplo de aplicação da heurística construtiva é apresentado. As propostas para trabalhos futuros são apresentadas no capítulo final desta dissertação. / For the past few years, hospitals have been forced to improve their productivity, with surgical centers being one of the sectors with higher costs within such organizations, but also the ones that generate the most revenue. Thus, optimization methods for surgical programming are tools that can be used to reduce queues and idleness in these sectors and consequently achieve the aforementioned goals. The \"Problem of Programming Multiple Surgical Resources with Multiple Steps\"consists in allocating the existing resources to each surgery stage that a patient will need to go through, considering the different needs, sequence and specificities of each of them, and then scheduling these steps in time. This type of problem is classified in the current literature as an NP-hard problem, being described as a Flexible Job Shop with blocking and an objective function that seeks to minimize the number of patients not served and the total makespan. The general purpose of this research is to propose a mathematical model and a constructive heuristic for this type problem. The proposed model explores the mathematical model Multi-Mode Blocking Job Shop (MMBJS) presented in Pham and Klikert (2008) suggesting improvements through the use of an alternative Mixed Integer Linear Programming that aims to: reduce the computational effort, adjust the makespan calculation and suggest a strategy of patients prioritization. In order to prove the benefits of the proposed enhancements, computational tests were performed to compare the MMJBS model and the proposed model, identifying that for instances where in which all patients are attended, the solutions found by CPLEX for both models are the same, but with a lower computational time the proposed model (45% average reduction). Also, other computational tests were performed to observe the behavior of the model with different configurations of resources. For instances with 15 patients, the tests indicate that the computational time to find the optimal solution is greater than 2 hours of processing. Thus a constructive heuristic is proposed, it aims to generate feasible solutions with little computational effort. The proposed heuristic allocates each surgery stage of a patient to the necessary resources, respecting the available windows and seeking to reduce the total slack in the system. An example of the application of the constructive heuristic is also presented. At last, future works proposals are presented in the final chapter of this dissertation.

O tema de roteamento de veículos é de grande importância na literatura e tem sido amplamente estudada pela sua importância para muitas indústrias. Com a evolução na literatura, mais características foram adicionadas para torná-lo mais próximo de situações reais. Alinhado com esta tendência, este trabalho aborda o problema de roteamento de veículos quando há a terceirização da frota que realiza as entregas. Uma forma de cobrança do frete é por meio de custos escalonados, que são calculados de acordo com o tipo de veículo e a distância percorrida, com valores fixos para cada faixa de distância. Embora seja uma forma comum de trabalho na indústria, nenhum trabalho focado nesta característica foi encontrado na literatura. Este problema é o problema de roteamento de veículos com frota mista, janelas de tempo e custos escalonados (FSMVRPTWSC). Ao abordar este problema, este trabalho apresenta um modelo de programação linear inteira mista que é avaliado em um cenário real da indústria. Além disso, três heurísticas de inserção sequencial são propostas para lidar com problemas maiores. Estes métodos são examinados por meio de testes computacionais em 168 problemas de referência gerados para este problema. Os experimentos numéricos mostram que os métodos são robustos e eficientes, apresentando um bom desempenho em conjuntos de problemas com diversas características. / The theme of vehicle routing is of great importance in the literature and has been widely studied for its relevance to many industries and, throughout the literature, more characteristics have been added to make it closer to real situations. Aligned with this trend, this paper addresses the vehicle routing problem when there is outsourcing of the fleet that delivers goods. One form of freight charging is by scaled costs, which are calculated according to the type of vehicle and the distance traveled, with fixed values for each distance range. Though it is a common form of work in the industry, no work focused on this characteristic was found in the literature. This problem is the fleet size and mix vehicle routing problem with time windows and scaled costs (FSMVRPTWSC). In approaching this problem, this paper presents a mixed integer linear programming model that is evaluated under a real situation scenario. Furthermore, three sequential insertion heuristics are proposed in order to deal with larger problems. These methods are examined through a computational comparative study in 168 benchmark problems generated for this problem. The numerical experiments show that the methods are robust and efficient, performing well in different problem sets.

O sequenciamento e a programação da produção trazem grandes benefícios financeiros às empresas se realizados de forma adequada. Atualmente, soluções generalizadas apresentam resultados aceitáveis, porém têm como consequência benefícios inferiores quando comparados a estudos específicos. O ramo da otimização de resultados possui dois tipos de soluções: as exatas para problemas de menores dimensões e não exatas, ou heurísticas, para problemas de médias e grandes dimensões. Este trabalho apresenta algoritmos exatos do tipo Branch & Bound e Modelos de Programação Linear Inteira Mista para solucionar quatro variações de problemas de scheduling: Fm|block|∑Cjm, Fm|block|∑Tj, Fm|block, Sijk|∑Cjm e Fm|block, Sijk|∑Tj. As abordagens utilizadas são inéditas na literatura e apresentaram resultados animadores para a maioria dos cenários. O limitante para o tempo total de fluxo obteve resposta ótima em 100% dos casos para problemas de até 20 tarefas e 4 máquinas em menos de uma hora. Para o tempo total de atraso, o limitante se mostrou mais eficiente quando os valores das due dates apresentam alta taxa de dispersão. Para os casos com setup, foram elaboradas três variações de limitantes para cada problema. O limitante com setup que apresentou o melhor desempenho foi o que obteve a melhor relação entre o seu valor numérico e seu custo computacional. Os modelos MILP solucionaram 100% dos problemas sem setup para até 20 tarefas e 4 máquinas e para os casos com setup, foram solucionados problemas de até 14 tarefas e 4 máquinas no tempo limite de uma hora. Os testes computacionais mostram a eficiência na redução do número de nós e, consequentemente, no tempo de execução. Portanto, o estudo realizado indica que, para problemas de pequeno porte e médio, os métodos em questão possuem grande potencial para aplicações práticas. / Job Sequence and Programming give benefits both financial and organizational to any company when performed properly. Nowadays, there is still a gap between theory and practice due to solutions that are short in specification. The analyzed problems differ in type and dimension thus modifying its complexity. The results optimization field is divided into two types of solution: the exact solution for minor problems and the non-exact solution for greater dimension problems. The present paper presents exact algorithms to solve the problems Fm|block|∑Cjm, Fm|block|∑Tj, Fm|block, Sijk|∑Cjm by the Branch & Bounds and Mixed Integer Linear Program models. The approaches are new and presented good results for most cases. Bounds for the no-setup total flow time scenario solved 100% of the 20 jobs and 4 machines cases. High dispersion range due dates contributed for the effectiveness of the no-setup total tardiness bound\'s effectiveness. Three different approaches were developed for the setup cases. The best approach aimed to optimize the value/effort factor for the B&B. The Mixed Integer Linear Program models solved 100% of the no-setup cases for 20 jobs and 4 machines. The MILPs setup cases solved optimally 14 jobs and 4 machines cases. Computational tests were executed and analyzed and they highlighted the node count reduction and, consequently, the execution time. The present study points out that the exact methods can be applied to small and medium scheduling problems in practice.

Orientador: John Fredy Franco Baquero / Resumo: A crescente penetração dos Veículos Elétricos (VEs) no setor de transportes representa um novo e grande desafio para o planejamento da expansão e da operação dos Sistemas de Distribuição de Energia Elétrica (SDEEs) devido ao correspondente aumento da demanda associada ao carregamento das baterias. Portanto, devem ser desenvolvidos métodos que ajudem os SDEEs a lidar com esses desafios, considerando as incertezas associadas às demandas convencionais e aos VEs. Nesta tese é proposto um método robusto baseado em um modelo de Programação Linear Inteira-Mista (PLIM) para auxiliar a integração de VEs no SDEE. O método proposto permite resolver o problema de planejamento multi-estágio da expansão do SDEE considerando a alocação e o dimensionamento de Estações de Carregamento de VEs (ECVEs). Restrições probabilísticas são usadas na formulação proposta para lidar com as incertezas associadas à demanda, garantindo o cumprimento da capacidade de potência das subestações com um nível de confiança especificado. O modelo proposto para o planejamento da expansão avalia a construção e/ou reforço de subestações, ECVEs e circuitos, assim como também a alocação de unidades de geração distribuída e bancos de capacitores ao longo do horizonte de planejamento. O modelo de PLIM proposto é resolvido através de técnicas de otimização clássica visando garantir a solução ótima do problema. A eficiência e robustez do modelo são verificadas usando sistemas teste de 18 e 54 nós, junto com simulações de Mo... (Resumo completo, clicar acesso eletrônico abaixo) / Abstract: The increasing penetration of electric vehicles (EVs) in the transportation sector represents a new challenge for the expansion planning of electrical distribution systems (EDS) due to the corresponding increase of the energy demand. Therefore, methods to support the EDS considering the uncertainties associated with conventional and EV demands should be developed. This thesis presents a methodology to consider the EV integration into the EDS. A mixed-integer linear programming (MILP) model is proposed to solve the multi-stage expansion planning of EDS considering the allocation and sizing of EV charging stations (EVCSs). Chance constraints are used in the formulation to deal with the uncertainties associated with the demands, guaranteeing the fulfilment of the substation capacities within a given confidence level. The proposed model for the expansion planning considers the construction/reinforce of substations, EVCSs and circuits as well as the allocation of distributed generation units and capacitor banks along the planning horizon. The proposed MILP model guarantees optimality using classical optimization techniques. The efficiency and robustness of the model is verified using two test systems with 18-nodes and 54-nodes. Monte Carlo simulations were carried out to verify the compliance of the proposed chance constraint. / Doutor

Orientador: Marcos Julio Rider Flores / Abstract: Electric distribution networks should be prepared to provide an economic and reliable service to all customers, as well as to integrate technologies related to distributed generation, energy storage, and plug-in electric vehicles. A proper representation of the electric distribution network operation, taking into account smart grid technologies, is key to accomplish these goals. This work presents mathematical formulations for the steady-state operation of electric distribution networks, which consider the unbalance of three-phase grids. Mathematical models of the operation of smart grid-related devices present in electric distribution networks are developed (e.g., volt-var control devices, energy storage systems, and plug-in electric vehicles). Furthermore, features related to the voltage dependency of loads, distributed generation, and voltage and thermal limits are also included. These formulations constitute a mathematical framework for optimization analysis of the electric distribution network operation, which could assist planners in decision-making processes. Different objectives related to technical and/or economic aspects can be pursued within the framework; in addition, the extension to multi-period and multi-scenario optimization is discussed. The presented models are built based on mixed integer linear programming formulations, avoiding the use of conventional mixed integer nonlinear formulations. The application of the presented framework is illustrated throughou... (Complete abstract click electronic access below) / Resumo: As redes de distribuição de energia elétrica devem estar preparadas para fornecer um serviço econômico e confiável a todos os clientes, bem como para integrar tecnologias relacionadas à geração distribuída, armazenamento de energia e veículos elétricos. Uma representação adequada da operação das redes de distribuição, considerando as tecnologias de redes inteligentes, é fundamental para atingir esses objetivos. Este trabalho apresenta formulações matemáticas para a operação em regime permanente das redes de distribuição, que consideram o desequilíbrio de redes trifásicas. Modelos matemáticos da operação de dispositivos relacionados à redes inteligentes presentes em redes de distribuição são desenvolvidos (e.g., dispositivos de controle volt-var, sistemas de armazenamento de energia e veículos elétricos). Além disso, características relacionadas à dependência da tensão das cargas, geração distribuída e limites térmico e de tensão também estão incluídos. Essas formulações constituem um marco matemático para a análise de otimização da operação das redes de distribuição de energia elétrica, o que possibilita modelar os processos de tomada de decisões. Objetivos diferentes relacionados a aspectos técnicos e/ou econômicos podem ser almejados dentro deste marco; Além disso, a extensão para otimização multi-período e multi-cenário é discutida. Os modelos apresentados são construídos com base em formulações de programação linear inteira mista, evitando o uso de formulações não-lineare... (Resumo completo, clicar acesso eletrônico abaixo) / Doutor

Submitted by Kamila Costa (kamilavasconceloscosta@gmail.com) on 2015-06-15T21:23:16Z No. of bitstreams: 1 Dissertacao-Alessandro B Trindade.pdf: 1833454 bytes, checksum: 132beb74daa71e138bbfcdc0dcf5b174 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-06-16T15:00:54Z (GMT) No. of bitstreams: 1 Dissertacao-Alessandro B Trindade.pdf: 1833454 bytes, checksum: 132beb74daa71e138bbfcdc0dcf5b174 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-06-16T15:02:16Z (GMT) No. of bitstreams: 1 Dissertacao-Alessandro B Trindade.pdf: 1833454 bytes, checksum: 132beb74daa71e138bbfcdc0dcf5b174 (MD5) / Made available in DSpace on 2015-06-16T15:02:16Z (GMT). No. of bitstreams: 1 Dissertacao-Alessandro B Trindade.pdf: 1833454 bytes, checksum: 132beb74daa71e138bbfcdc0dcf5b174 (MD5) Previous issue date: 2015-02-09 / Não Informada / When performing hardware/software co-design for embedded systems, does emerge the problem of allocating properly which functions of the system should be implemented in hardware (HW) or in software (SW). This problem is known as HW/SW partitioning and in the last ten years, a significant research effort has been carried out in this area. In this proposed project, we present two new approaches to solve the HW/SW partitioning problem by using SMT-based verification techniques, and comparing the results using the traditional technique of Integer Linear Programming (ILP) and a modern method of optimization by Genetic Algorithm (GA). The goal is to show with experimental results that model checking techniques can be effective, in particular cases, to find the optimal solution of the HW/SW partitioning problem using a state-of-the-art model checker based on Satisfiability Modulo Theories (SMT) solvers, when compared to the traditional techniques. / Quando se realiza um coprojeto de hardware/software para sistemas embarcados, emerge o problema de se decidir qual função do sistema deve ser implementada em hardware (HW) ou em software (SW). Este tipo de problema recebe o nome de particionamento de HW/SW. Na última década, um esforço significante de pesquisa tem sido empregado nesta área. Neste trabalho, são apresentadas duas novas abordagens para resolver o problema de particionamento de HW/SW usando técnicas de verificação formal baseadas nas teorias do módulo da satisfabilidade (SMT). São comparados os resultados obtidos com a tradicional técnica de programação linear inteira (ILP) e com o método moderno de otimização por algoritmo genético (GA). O objetivo é demonstrar, com os resultados empíricos, que as técnicas de verificação de modelos podem ser efetivas, em casos particulares, para encontrar a solução ótima do problema de particionamento de HW/SW usando um verificador de modelos baseado no solucionador SMT, quando comparado com técnicas tradicionais.