2017_11_30 Hitzaldia/Charla: SAT y SMT para problemas combinatorios

Hizlaria /Ponente:  Mateu Villaret Auselle (Universitat de Girona)
Izenburua/Título:
   SAT y SMT para problemas combinatorios
Hizkuntza/idioma: Gaztelania/Castellano
Data/Fecha:               2017/11/30
Ordua/ Hora:           11:00
Tokia/Lugar:           Ada Lovelace aretoa, Informatika fakultatea UPV/EHU
Antolatzaileak / Organizadores:       Lorea & Ufi Bailab

 [EU]

Laburpena:

Problema konbinatorioak gure eguneroko bizitzaren zati dira. Ikastetxeetako ordutegien prestaketak edo eginkizunen programazio efizienteak, hala nola patata frijituak paketatzeak edo sudokuen gisako denbora-pasek, berezko konplexutasun handia dute, eta denbora esponentzial bat behar izaten dute ebazteko. Problema multzo horren barne SAT aurkitzen dugu: formula proposizional bat betegarria den erabakitzeko problema.

SATen adierazkortasunak beste problema konplexu batzuk hartara murriztu ahal izatea errazten du. Gainera, azken urteetan ikertzaile askoren arreta erakarri du, eta gaur egun milaka klausula eta aldagai dituzten formulak ebazteko gai diren SAT-solver direlakoak azaldu dira.

Hitzaldi honen lehen zatian SAT zer den, SAT-solver-en osagai nagusiak zein diren eta SATen hedapen nagusietako bat zertan datzan azalduko dugu: SAT modulu teoriak delakoa (SMT).

Hitzaldiaren bigarren zatian, problema konbinatorio horiek ebazteko SAT eta SMT nola erabili ditugun azalduko dugu, bereziki zereginen programazio eraginkorraren problema eta modulu teoriak planifikazio-arena.

Curriculum laburra:

Mateu Villaret Gironako Unibertsitateko Professor Agregat da. Unibertsitate horretako Logic & Programming (LAP) ikertaldearen arduraduna izan da 5 urtez. Bere ikerketa logika konputazionalaren inguruan kokatzen da, hasieran dedukzio automatikoaren esparruan, eta azken aldian, problema konbinatorio zailak ebazteko erabiliz. Ikerketa horren fruitu dira izen handiko nazioarteko berrogeita hamar argitalpen, hogeita hamar kolaboratzaile baino gehiagorekin egindakoak.

Universitat Politècnica de Catalunya-n doktore da. Hainbat doktoretza-tesi zuzendu ditu. Horien emaitza dira hainbat tresna lehiakor, hala nola Rantanplan, zenbakizko planifikazioko problemetarako, eta rcpsp2smt zereginen programazioko proble-metarako.

 [ES]

Resumen:

Los problemas combinatorios forman parte de nuestra vida cotidiana. Tanto la confección de horarios en centros educativos, o la programación eficiente de tareas, como el empaquetado de patatas fritas o la resolución de pasatiempos como los sudokus, esconden una complejidad intrínseca extraordinaria que puede requerir de un tiempo exponencial para su resolu-ción. Dentro de esta familia de problemas se encuentra SAT: el problema de decidir si una fórmula proposicional es satisfactible.

La expresividad de SAT hace fácil que se puedan reducir otros problemas complejos a él. Además, en los últimos años ha captado la atención de un gran número de investiga- dores, haciendo que hoy en día existan SAT-solvers capaces de resolver fórmulas con centenares de miles de cláusulas y variables.

En la primera parte de esta charla explica- remos qué es SAT, cuáles son los principales ingredientes de los SAT-solvers y en qué consiste una de las principales extensiones de SAT: SAT módulo teorías (SMT).
En la segunda parte de la charla, explicaremos como hemos utilizado SAT y SMT para resolver dichos problemas combinatorios, en particular el de programación eficiente de tareas y el de planificación módulo teorías.

Mateu Villaret (CV):

Mateu Villaret es Professor Agregat en la Universitat de Girona. Ha sido durante cinco años responsable del grupo de investigación Logic & Programming (LAP) de dicha universidad. Su investigación se enmarca en el entorno de la lógica computacional, ini- cialmente en el ámbito de la deducción automática y últimamente usándola para resolver problemas combinatorios difíciles. Esta investigación se ha concretado en unas cincuenta publicaciones internacionales de prestigio con más de treinta colaboradores.

Es doctor por la Universitat Politècnica de Catalunya. Ha dirigido varias tesis doctora- les fruto de las cuales han surgido diferentes herramientas competitivas como son Rantanplan para problemas de planificación numérica y rcpsp2smt para problemas de programación de tareas.

Iruzkin bat honentzako: 2017_11_30 Hitzaldia/Charla: SAT y SMT para problemas combinatorios

Erantzuna idatzi

 

 

 

HTML etiketa hauek erabil ditzakezu

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>