Boolean satisfiability problem

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable. SAT is the first problem that was proven to be NP-complete; see Cook–Levin theorem. This means that all

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (57)

Related publications

Related people (11)

Related people

Related units (5)

Related units

Related concepts (59)

Related concepts

Related courses (14)

Related courses

Related lectures (27)

Related lectures

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

COM-516: Markov chains and algorithmic applications

The study of random walks finds many applications in computer science and communications. The goal of the course is to get familiar with the theory of random walks, and to get an overview of some applications of this theory to problems of interest in communications, computer and network science.

ME-371: Discretization methods in fluids

Ce cours présente une introduction aux méthodes d'approximation utilisées pour la simulation numérique en mécanique des fluides. Les concepts fondamentaux sont présentés dans le cadre de la méthode des différences finies puis étendus à celles des éléments finis et spectraux.

Computational complexity theory

In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each ot

P versus NP problem

The P versus NP problem is a major unsolved problem in theoretical computer science. In informal terms, it asks whether every problem whose solution can be quickly verified can also be quickly solve

NP-completeness

In computational complexity theory, a problem is NP-complete when:

It is a decision problem, meaning that for any input to the problem, the output is either "yes" or "no".

When the answer is "ye

Asynchronous updates for stochastic gradient descent

Alberto Silvio Chiappa

Finding convergence rates for numerical optimization algorithms is an important task, because it gives a justification to their use in solving practical problems, while also providing a way to compare their efficiency. This is especially useful in an asynchronous environment, because the algorithms are often proven to be more efficient than their synchronous counterparts by experience, but they lack the theory that justifies this property. Furthermore, analyzing the various issues that can arise when inconsistency is taken into consideration, it is possible to obtain a clearer picture of the downsides of inexact implementations one should be aware of. This work tries to address the problem of finding an expected convergence rate for the asynchronous version of the widely popular stochastic gradient descent algorithm, applied to the common class of problems that present a cost function with a sum structure. It follows a similar approach to the one suggested by R. Leblond, F. Pedregosa and S. Lacoste-Julien in "ASAGA: Asynchronous Parallel SAGA" (2016) [RLLJ16], also borrowing their formalization of asynchronicity. The main achievement of this work is a bound on the constant step size that guarantees convergence in expectation of the algorithm. The relative convergence rate is also obtained. The result is also partially validated by sequential models of an asynchronous environment. We hope that this can be a basis for future applications of the same approach to more specific algorithms and that numerical experiments on real multiprocessor architecture can be performed in the future to further validate the convergence rates.

2017

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragment is independentof the base element and index set theories.

Springer, Cham2022

Simulation numérique des phénomènes thermiques et magnétohydrodynamiques dans une cellule de Hall-Héroult

Yasser Safa

This work is concerned with a numerical simulation of the thermal behaviour of an electrolysis cell for the production of the aluminium. Aluminium is produced by an electrolytic reduction of alumina dissolved in a bath of molten cryolite. In this reduction process, called Hall-Héroult process, the metal is produced at about 965 °C. A frozen bath layer, called ledge, arises in the boundary region and protects the side walls of the cell from corrosive electrolyte. This ledge may change the magnetohydrodynamical equilibrium of the cell and reduce the heat loss through the walls. The ledge is thus playing a significant role in both the thermal and magnetohydrodynamical behaviour of the cell. A precise knowledge of the ledge is thus an imporant ingredient in the optimization process of the cell. The temperature field and the ledge shape in a whole smelter are obtained by simultaneously solving the system of equations formed by: a non-linear convection-diffusion heat equation, which can be considered as a Stephan problem in enthalpy and temperature in the domain of the cell occupied by fluids and ledge, Navier-Stokes equations with a free interface in the fluid domains and Maxwell equations in the whole space. The source term of the heat equation results from the Joule effect due to the electrical current crossing the cell. A Chernoff scheme is used to numerically solve Stephan problem. Three dimensional numerical calculations showing ledge shape, temperature and velocity fields as well as electrical potential for an operating cell are obtained. The effect of thermal field on the electrical current and the effect of fluid motions on the ledge shape in the aluminium cells are presented.

EPFL2005