Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Challenges in Bit-Precise Reasoning

Description

This lecture by the instructor from Johannes Kepler University, Linz, Austria, at FMCAD 2014 discusses challenges in bit-precise reasoning, including SMT-COMP results, AIG, bit-blasting, Tseitin transformation, Boolector architecture, and complexity classes. It covers topics like bit-wise operators, shifting, dual propagation, and model checking.

Official source

Ontological neighbourhood

Theoretical computer science

Theory of computation: Computational complexity theory

Related concepts (32)

Complexity class

In computational complexity theory, a complexity class is a set of computational problems "of related resource-based complexity". The two most commonly analyzed resources are time and memory. In general, a complexity class is defined in terms of a type of computational problem, a model of computation, and a bounded resource like time or memory. In particular, most complexity classes consist of decision problems that are solvable with a Turing machine, and are differentiated by their time or space (memory) requirements.

NP (complexity)

In computational complexity theory, NP (nondeterministic polynomial time) is a complexity class used to classify decision problems. NP is the set of decision problems for which the problem instances, where the answer is "yes", have proofs verifiable in polynomial time by a deterministic Turing machine, or alternatively the set of problems that can be solved in polynomial time by a nondeterministic Turing machine. NP is the set of decision problems solvable in polynomial time by a nondeterministic Turing machine.

Parameterized complexity

In computer science, parameterized complexity is a branch of computational complexity theory that focuses on classifying computational problems according to their inherent difficulty with respect to multiple parameters of the input or output. The complexity of a problem is then measured as a function of those parameters. This allows the classification of NP-hard problems on a finer scale than in the classical setting, where the complexity of a problem is only measured as a function of the number of bits in the input.

P (complexity)

In computational complexity theory, P, also known as PTIME or DTIME(nO(1)), is a fundamental complexity class. It contains all decision problems that can be solved by a deterministic Turing machine using a polynomial amount of computation time, or polynomial time. Cobham's thesis holds that P is the class of computational problems that are "efficiently solvable" or "tractable". This is inexact: in practice, some problems not known to be in P have practical solutions, and some that are in P do not, but this is a useful rule of thumb.

Model checking

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash). In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language.

Related lectures (42)

Elements of Computational Complexity

Introduces computational complexity, decision problems, quantum complexity, and probabilistic algorithms, including NP-hard and NP-complete problems.

Complexity of Algorithms: Big-O Notation

Explores algorithm complexity, big-O notation, induction, recursion, and analysis of running times, covering NP problems and complexity classes.

Complexity Classes: Introduction and Examples MOOC: Information, Computation, Communication: Introduction to computational thinking

Introduces complexity classes, including P and NP, and explores examples of easy and hard problems.

Understanding Complexity: Algorithms and NP Problems

Covers complexity classes, tractable problems, the class NP, NP-complete problems, and summarizes the concept of tractable problems.

Complexity & Induction: Algorithms & Proofs