Seminário

A refutation system for Satisfiability beyond Conflict-driven clause learning and Resolution

Sala 6.2.44, FCUL, Lisboa

Por Maria Luisa Bonet (Universidad Politecnica de Catalunya).

Abstract: The problem of Satisfiability (SAT) is NP-complete, and therefore hard to solve. On the other and, it is very important to find the best algorithms to solve as many instances of SAT as possible, since many important real life problems can be encoded into SAT. Conflict-driven clause learning (CDCL) is at the core of the success of modern SAT solvers. In terms of propositional proof complexity, CDCL has been shown as strong as the propositional proof system of general resolution.

Improvements to SAT solvers can be realized either by improving existing algorithms, or by exploiting proof systems stronger than CDCL.It is open whether a proof system stronger than CDCL/RES could yield more efficient SAT solvers, as attempts at exploiting extended resolution or cutting planes in SAT solvers have been so far largely unsuccessful.

Furthermore, a key issue from a practical perspective is whether proof systems are automatizable. A proof system is automatizable, if there is an algorithm that finds proofs in that system, in time polynomial in the smallest proofs of the tautology. Unfortunately, most results regarding automatizability are negative (Bonet-Pitassi-Raz, Razborov).

Recent work (Ignatiev-Morgado-Marques-Silva) proposed an approach for solving SAT by an encoding to Horn MaxSAT. The proposed reduction coupled with MaxSAT resolution represents a new proof system, DRMaxSAT, which was shown to enable polynomial time refutations of pigeonhole formulas, in contrast with  either CDCL or general resolution.

The work of Bonet-Buss-Ignatiev-Marques-Silva-Morgado) investigates the DRMaxSAT proof system, and shows that DRMaxSAT p-simulates general resolution, that AC_0-Frege+PHP p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate neither AC^0-Frege+PHP nor the cutting planes proof system.

Short Bio: Maria Luisa Bonet obtained a Ph.D. in Mathematics at the University of California, Berkeley, under the joint direction of Leo Harrington and Sam Buss. She held the Warshowsky assistant professorship at University of California, San Diego, and a two year postdoc at the University of Pennsylvania. Currently she is a full professor in Computer Science, at the Universidad Politecnica de Catalunya.

10h00
Departamento de informática
Título "Bolsas de Doutoramento Unite! ULisboa", logótipos das entidades promotoras e fotografia de jovem investigadora a utilizar um laptop na esplanada de um café

O 3.º concurso decorre de 29 de março a 30 de abril.

A atividade consiste numa caminhada pelo Lousal, passando por vários pontos importantes da história da Mina do Lousal.

BioISI Research Seminar, por Duarte Figueiredo (Max Planck Institute of Molecular Plant Physiology).

Alunos de Ciências

Uma iniciativa gratuita, dirigida aos estudantes do 1.º Ciclo de estudos de Ciências ULisboa.

Título/data/local do evento, logótipo da RedeMov e fotografia de autocarro

Evento no âmbito do Ciclo de Conferências "Conversas à 6.ª", promovido pela redeMOV da Universidade de Lisboa.

Logótipo do programa e pormenor de comboio

Pronto para embarcar numa mobilidade sustentável e numa aventura multicultural?

Geometry and Physics Seminar / Theory of Computing Seminar por Florian Pausinger (Queen's University Belfast).

Título do evento e representação de rosto humano

An interdisciplinary workshop that brings together world-leading scholars, junior researchers, artists, clinicians and more importantly people with lived experiences of Depersonalisation to address key questions around this widely spread yet under-acknowledged condition.

Composição do logótipo da ULisboa e de representação do rosto humano à base de relógios

Consegue comunicar eficazmente a sua investigação de doutoramento em 3 minutos?

Ao longo das 30 horas deste curso, serão abordados temas, tais como contornar as principais dificuldades na comunicação da Biodiversidade, como usar histórias, ou a importância dos conceitos científicos na hora de os comunicar.

Título/data/local do evento

O evento visa mobilizar atores nacionais nas missões europeias do Horizonte Europa que contribuem para o Pacto Ecológico Europeu.

Pormenor da exposição e data da visita guiada

Visita guiada pela autora da exposição, Inez Wijnhorst, e o seu curador, Pedro Freitas (CIUHCT), apresentando duas visões - a artística e a matemática - que se complementam.

Fotografia de participantes numa anterior edição da Jobshop Ciências

O maior evento de empregabilidade de Ciências, a decorrer nos dias 09 e 10 de abril.

Título do programa, sobre um fundo azul escuro

Candidaturas até 31 de março.

Título do evento e mosaico de imagens (feixe de luz e silhueta humana)

Estás pronto para alavancar o teu conhecimento e abrir novas oportunidades profissionais?

Título/data/local do evento

An advanced worshop organised by 3D-BioInfo-PT, the community of Portuguese scientific researchers working in fields connected to Structural Bioinformatics.

The conference aims to bring together students and young researchers working in Mathematics, Statistics, and Applications with a view to fostering discussions and collaborations amongst participants.

Logótipos do Concurso Nacional para Jovens Cientistas e Investigadores e da Fundação da Juventude

Candidaturas até 15 de abril.

Seminário Helena Avelar de Astronomia e Astrologia Antiga, por Levente László (Eötvös University).

Logótipo de Ciências ULisboa, título "Dia de Ciências 2024" e frase apelando à participação

23 de abril. Virgínia Dignum, especialista Nações Unidas para IA, é oradora convidada.

O encontro reúne cientistas, profissionais e estudantes de diferentes áreas e regiões do país focados em desenvolver a investigação marinha, em linha com a Década da Ciência Oceânica para o Desenvolvimento Sustentável, proclamada pelas Nações Unidas (2021-2030).

Logótipo da ação CLEANFOREST

Forests are exposed to multiple global change drivers, wich can constrain their ability to continue providing several ecosystem services (including climate change mitigation). Assessing responses - and underlined mechanisms -  at the whole ecosystem scale is paramount for a holistic understanding of forest response to global change.

Título e data do evento, inseridos em fotografia de cinco jovens em contexto de investigação

Pré-inscrições já disponíveis!

Título do curso

Curso Avançado CEAUL / Gades Solutions.

Logótipo do EVM 2024

Candidaturas até 15 de maio.

Páginas