Sets with Cardinality Constraints in Satisfiability Modulo Theories

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 present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assum ...

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 ...

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

Logic rewriting is a powerful optimization technique that replaces small sections of a Boolean network with better implementations. Typically, exact synthesis is used to compute optimum replacement on-the-fly, with possible support for Boolean don't cares. ...

Technology mapping transforms a technology-independent representation into a technology-dependent one given a library of cells. This process is performed by means of local replacements that are extracted by matching sections of the subject graph to library ...

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 consider the problem of comparing several samples of stochastic processes with respect to their second-order structure, and describing the main modes of variation in this second order structure, if present. These tasks can be seen as an Analysis of Vari ...

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

Security system designers favor worst-case security metrics, such as those derived from differential privacy (DP), due to the strong guarantees they provide. On the downside, these guarantees result in a high penalty on the system's performance. In this pa ...

An integer linear program is a problem of the form max{c^T x : Ax=b, x >= 0, x integer}, where A is in Z^(n x m), b in Z^m, and c in Z^n. Solving an integer linear program is NP-hard in general, but there are several assumptions for which it becomes fixed ...

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 ...

The popular isolation level multiversion Read Committed (RC) exchanges some of the strong guarantees of serializability for increased transaction throughput. Nevertheless, transaction workloads can sometimes be executed under RC while still guaranteeing se ...

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 ...

Omnidirectional video streaming is usually implemented based on the representations of tiles, where the tiles are obtained by splitting the video frame into several rectangular areas and each tile is converted into multiple representations with different r ...

Minimising the longest travel distance for a group of mobile robots with interchangeable goals requires knowledge of the shortest length paths between all robots and goal destinations. Determining the exact length of the shortest paths in an environment wi ...

This paper studies the problem of online performance optimization of constrained closed-loop control systems, where both the objective and the constraints are unknown black-box functions affected by exogenous time-varying contextual disturbances. A primal- ...

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 fragme ...

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

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 present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We use as a base a variation of Hopcroft, Ullman and Aho algorithm for tree isomo ...

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Chat with Graph Search

Mechanized HOL Reasoning in Set Theory

Orthologic with Axioms

Interpolation and Quantifiers in Ortholattices

Scalable Logic Rewriting Using Don’t Cares

In Medio Stat Virtus: Combining Boolean and Pattern Matching

Succinct ordering and aggregation constraints in algebraic array theories

Transportation-based functional ANOVA and PCA for covariance operators

LISA – A Modern Proof System

Bayes Security: A Not So Average Metric

Results on Sparse Integer Programming and Geometric Independent Sets

Extractable Witness Encryption for the Homogeneous Linear Equations Problem

When is it safe to run a transactional workload under Read Committed?

Approximation Algorithms for Allocation and Network Design

Quality-Constrained Encoding Optimization for Omnidirectional Video Streaming

Certification of Bottleneck Task Assignment With Shortest Path Criteria

Primal-Dual Contextual Bayesian Optimization for Control System Online Optimization with Time-Average Constraints

NP Satisfiability for Arrays as Powers

Formula Normalizations in Verification

Scaling Language Features for Program Verification

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time