{"id":88257,"date":"2018-03-10T00:13:12","date_gmt":"2018-03-10T00:13:12","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/systematic-and-local-search-algorithms-for-regular-sat\/"},"modified":"2018-03-10T00:13:12","modified_gmt":"2018-03-10T00:13:12","slug":"systematic-and-local-search-algorithms-for-regular-sat","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/systematic-and-local-search-algorithms-for-regular-sat\/","title":{"rendered":"Systematic and local search algorithms for regular-sat"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Ramon Bejar Torres <\/strong><\/h2>\n<p>Regular-sat es el problema de decidir la satisfactibilidad de una clase de f\u00f3rmulas proposicionales multivaluadas llamadas f\u00f3rmulas cnf regulares. una f\u00f3rmula cnf regular es una forma normal conjuntiva cl\u00e1sica basada en una noci\u00f3n generalizada de literal, llamada literal regular. Dado un conjunto de valores de verdad n, con al menos dos valores de verdad, equipado con un orden total, un literal regular es una expresi\u00f3n de la forma s:p, donde p es una variable proposicional y s es un subconjunto de n el cual es o de la forma   i o de la forma   i, para alg\u00fan i de n. Una interpretaci\u00f3n multivaluada dada satisface un literal regular s:p sii asigna i de n. Una interpretaci\u00f3n multivaluada dada satisface un literal regular s:p sii asigna a p un valor de verdad de s, y satisface una cl\u00e1usula regular sii satisface al menos uno de sus literales. Una f\u00f3rmula cnf regular es satisfactible sii existe una interpretaci\u00f3n que satisface todas sus cl\u00e1usulas, en caso contrario, es insatisfactible.  en esta tesis nos centramos en el dise\u00f1o, implementaci\u00f3n y an\u00e1lisis de algoritmos de b\u00fasqueda sistem\u00e1tica y local para regular-sat, y definimos un m\u00e9todo generico para resoluci\u00f3n de problemas el cual consiste en modelar problemas combinatorios como instancias de regular-sat y entonces resolver las f\u00f3rmulas resultantes con algoritmos para regular-sat. En particular, prestamos especial atenci\u00f3n a la definici\u00f3n de estructuras de datos adecuadas para representar f\u00f3rmulas, heur\u00edsticas para explorar eficientemente el espacio de b\u00fasqueda, estrategias para escapar de m\u00ednimos locales en algoritmos de busqueda local, y codificaciones adecuadas basadas en regular-sat para modular problemas combinatorios.  en lo concerniente a algoritmos de b\u00fasqueda sistem\u00e1tica hemos dise\u00f1ado e implementado una variante de regular-dp, el cual es un algoritmo estilo davis-putnam para f\u00f3rmulas cnf regulares. Respecto a algoritmos de b\u00fasqueda local hemos dise\u00f1a<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Systematic and local search algorithms for regular-sat<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Systematic and local search algorithms for regular-sat <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Ramon Bejar Torres <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Aut\u00f3noma de barcelona<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 21\/12\/2000<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Felip Manya Serres<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: francesc Esteva massager <\/li>\n<li>carla Pedro gomes (vocal)<\/li>\n<li>reiner M\u00ed\u00a4hnle (vocal)<\/li>\n<li> Del val latorre \u00c1lvaro (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Ramon Bejar Torres Regular-sat es el problema de decidir la satisfactibilidad de una clase de f\u00f3rmulas proposicionales [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[1890,2528,126],"tags":[184272,120230,40763,175002,184271,184273],"class_list":["post-88257","post","type-post","status-publish","format-standard","hentry","category-ciencia-de-los-ordenadores","category-inteligencia-artificial","category-matematicas","tag-carla-pedro-gomes","tag-del-val-latorre-alvaro","tag-felip-manya-serres","tag-francesc-esteva-massager","tag-ramon-bejar-torres","tag-reiner-mihnle"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/88257","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=88257"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/88257\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=88257"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=88257"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=88257"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}