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.

Departamento de informática

Talk @LASIGE, por Catarina Gamboa (LASIGE/FCUL and ISR/CMU).

Apresentação por Luís Correia (Ciências ULisboa), no âmbito da pré-programação da IBERAMIA 2022 - 17th Ibero-American Conference on Artificial Intelligence.


Philosophical metatheories have had a great development in recent times. They have been used to reconstruct theories in many different scientific fields, from physics to biology to the social sciences. However, they lack means to systematically test the adequacy of their products.

Seminário do Centro de Física Teórica e Computacional, por Artem Ryabov (Charles University, Prague, Czech Republic).


Um programa dirigido aos alunos de Licenciatura e de 1.º ano de Mestrado.

Logótipo do evento

O conceito de One Health assenta no reconhecimento da necessidade de abordar as políticas de saúde numa perspetiva de interdependência humano-animal-ambiente.

Cognitive sciences have approached social cognition from two complementary perspectives. On one hand, social psychology and behavioural economics have mostly emphasized mentalizing, social perception, and our ability to model other minds. On the other hand, developmental psychology and motor neuroscience have more focused on imitating, social interaction, and our propensity to coordinate with others’ behaviour. 

The course aims at enabling the participants to use different methods to measure the impacts of pollutants on ecosystems. Basic knowledge will be provided through theoretical and practical lessons on how to select and use the most suitable metrics based on the analysis of multiple compartments of the ecosystems.

Logótipo e data do evento

“There is often a considerable difference between what we think people need and what people want to use”. This is our perspective on how technology should be developed and will serve as the motto of this event.

O evento visa reunir investigadores interessados na aplicação de isótopos estáveis em estudos ecológicos e na utilização de dados históricos de biodiversidade disponíveis em coleções museológicas.

Mathematical Cultures Seminar, por Henrique Leitão (DHFC Ciências ULisboa/CIUHCT).

Título e data do evento, sobre uma fotografia da Ponte Vasco da Gama (Lisboa)

O evento decorre de 12 a 14 de julho de 2022, sob o lema CHEMISTRY: Forging bonds, e destina-se a todos os investigadores e alunos da ULisboa.

Banner do evento

David Avelar (Ciências ULisboa) é um dos oradores do webinário.

Banner do evento

The program will consist of plenary lectures, oral, flash and poster communications, and a round table about Science Communication.

This course offers an overview of the different ways to measure biodiversity, and provides tips for the stratification of primary biodiversity data and the construction of variables that describe its various facets. It also includes an in-depth review of the different types of data used to measure biodiversity and their problems and limitations.

Banner do evento

Estaremos hoje habilitados a prever o impacto da atividade humana no clima e a inferir daí a insustentabilidade do nosso modo de vida?

Logótipo do programa

Após 2 anos de interregno, o programa Ser Cientista está de regresso!

Imagem alusiva ao prémio

Candidaturas até 31 de julho.

Fotografia de campo agrícola e parque eólico

Submissão de iniciativas até 30 de agosto de 2022.

Fotografia de trator em campo agrícola

Submissão de iniciativas até 30 de agosto de 2022.

Fotografia representativa de agricultura sustentável

Submissão de iniciativas até 30 de agosto de 2022.

Programa a disponibilizar futuramente.