NP Satisfiability for Arrays as Powers

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

We discuss two extensions to a recently introduced theory of arrays, which are based on considerations coming from the model theory of power structures. First, we discuss how the ordering relation on the index set can be expressed succinctly by referring t ...

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

In this thesis, we give new approximation algorithms for some NP-hard problems arising in resource allocation and network design. As a resource allocation problem, we study the Santa Claus problem (also known as the MaxMin Fair Allocation problem) in which ...

Dataflow programming is a methodology that enables the development of high-level, parametric programs that are independent of the underlying platform. This approach is particularly useful for heterogeneous platforms, as it eliminates the need to rewrite ap ...

Witness encryption is a cryptographic primitive which encrypts a message under an instance of an NP language and decrypts the ciphertext using a witness associated with that instance. In the current state of the art, most of the witness encryption construc ...

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

We consider fundamental algorithmic number theoretic problems and their relation to a class of block structured Integer Linear Programs (ILPs) called 2-stage stochastic. A 2-stage stochastic ILP is an integer program of the form min{c(T)x vertical bar Ax = ...

We show that Cutting Planes (CP) proofs are hard to find: Given an unsatisfiable formula F, It is -hard to find a CP refutation of F in time polynomial in the length of the shortest such refutation; and unless Gap-Hitting-Set admits a nontrivial algorithm, ...

Many natural optimization problems are NP-hard, which implies that they are probably hard to solve exactly in the worst-case. However, it suffices to get reasonably good solutions for all (or even most) instances in practice. This paper presents a new algo ...

Modelling and analysis of biological systems is crucial in order to quantitatively explain and predict their behaviour. The importance of modelling in systems biology becomes even more evident when tackling complex, large systems. Approaches that rely on ...

We study different symbolic algorithms to solve two related reconfiguration problems on graphs: the token swapping problem and the permutation routing via matchings problem. Input to both problems is a connected graph with labeled vertices and a token in e ...

Landslide-generated waves, also called impulse waves, occur as a result of the intrusion of landslides (such as rock falls, debris flows, and avalanches) into bodies of water (such as lakes, reservoirs, and seas). The objective of this thesis was to study ...

Recent studies show that majority-based logic synthesis is beneficial for both traditional and nanotechnology digital designs. However, most of the existing synthesis algorithms for majority logic generate majority-of-three (M-3) networks. The optimization ...

Today, the design of electronic systems is largely automated. The practice of using software automation technologies for the design of electronic hardware is commonly referred to as Electronic Design Automation (EDA). EDA comprises a large set of tools, fr ...

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

Vulnerability metrics play a key role in the understanding of cascading failures and target/random attacks to a network. The graph fragmentation problem (GFP) is the result of a worst-case analysis of a random attack. We can choose a fixed number of indivi ...

Designing digital circuits well is notoriously difficult. This difficulty stems in part from the very many degrees of freedom inherent in circuit design, typically coupled with the need to satisfy various constraints. In this thesis, we demonstrate how for ...

A representation of a Boolean function is canonical if, given a variable order, only one instance of the representation is possible for the function. A computation is canonical if the result depends only on the Boolean function and a variable order, and do ...

In this paper, we discuss recent advances in exact synthesis, considering both their efficient implementation and various applications in which they can he employed. We emphasize on solving exact synthesis through Boolean satisfiability (SAT) encodings. Di ...

Optimization is a fundamental tool in modern science. Numerous important tasks in biology, economy, physics and computer science can be cast as optimization problems. Consider the example of machine learning: recent advances have shown that even the most s ...

NP Satisfiability for Arrays as Powers

Chat with Graph Search

Succinct ordering and aggregation constraints in algebraic array theories

Orthologic with Axioms

Approximation Algorithms for Allocation and Network Design

Design Space Exploration for Partitioning Dataflow Program on CPU-GPU Heterogeneous System

Extractable Witness Encryption for the Homogeneous Linear Equations Problem

Scaling Language Features for Program Verification

The double exponential runtime is tight for 2-stage stochastic ILPs

Automating cutting planes is NP-hard

Learning from survey propagation: a neural network for MAX-E-3-SAT

Modelling the Intracellular Environment under Uncertainty, from Post-translational Modification to Metabolic Networks

Symbolic Algorithms for Token Swapping

Experimental study of impulse waves generated by viscoplastic fluid

Exact Synthesis of Boolean Functions in Majority-of-five Forms

SAT-Based Exact Synthesis for Multi-Level Logic Networks

Verified Functional Programming

Graph fragmentation problem: analysis and synthesis

Satisfiability-Based Methods for Digital Circuit Design, Debug, and Optimization

Canonical Computation without Canonical Representation

Practical Exact Synthesis

New Algorithmic Paradigms for Discrete Problems using Dynamical Systems and Polynomials