Publication

On Deciding Functional Lists with Sublist Sets

Related publications (88)

Graph Chatbot

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.

A Sound and Complete Axiomatization of Majority-n Logic

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù, Anupam Chattopadhyay

Manipulating logic functions via majority operators recently drew the attention of researchers in computer science. For example, circuit optimization based on majority operators enables superior results as compared to traditional logic systems. Also, the B ...

Institute of Electrical and Electronics Engineers2016

On Satisfiability for Quantified Formulas in Instantiation-Based Procedures

Viktor Kuncak, Nicolas Charles Yves Voirol

Procedures for first-order logic with equality are used in many modern theorem provers and solvers, yet procedure termination in case of interesting sub-classes of satisfiable formulas remains a challenging problem. We present an instantiation-based semi-d ...

2016

Fast generation of lexicographic satisfiable assignments: enabling canonicity in SAT-based applications

Giovanni De Micheli, Paolo Ienne, Mathias Soeken, Ana Petkovska

Lexicographic Boolean satisfiability (LEXSAT) is a variation of the Boolean satisfiability problem (SAT). Given a variable order, LEXSAT finds a satisfying assignment whose integer value under the given variable order is minimum (maximum) among all satisfi ...

Assoc Computing Machinery2016

Multi-Label Answer Aggregation for Crowdsourcing

Thành Tâm Nguyên

Crowdsourcing has been widely established as a means to enable human computation at large scale, in particular for tasks that require manual labelling of large sets of data items. Answers obtained from heterogeneous crowd workers are aggregated to obtain a ...

2016

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Andrew Joseph Reynolds

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...

Springer-Verlag Berlin2015

Sampling Curves with Finite Rate of Innovation

Thierry Blu, Hanjie Pan, Pier Luigi Dragotti

In this paper, we extend the theory of sampling signals with finite rate of innovation (FRI) to a specific class of two-dimensional curves, which are defined implicitly as the zeros of a mask function. Here the mask function has a parametric representation ...

Institute of Electrical and Electronics Engineers2014

Verifying and Synthesizing Software with Recursive Functions (Invited Contribution)

Viktor Kuncak

Our goal is to help people construct software that does what they wish. We develop tools and algorithms that span static and dynamic verification, constraint solving, and program synthesis. I will outline the current state our verification and synthesis sy ...

Springer-Verlag Berlin2014

, , ,

A determination is made regarding whether to merge two symbolic analysis states. A first state corresponds to a first path through a program to a program location and a second state corresponds to a second path through the program to the program location. ...

2013

, ,

By a polygonization of a finite point set S in the plane we understand a simple polygon having S as the set of its vertices. Let B and R be sets of blue and red points, respectively, in the plane such that is in general position, and the convex hull of B c ...

Springer Japan2013

We present CafeSat, a SAT solver written in the Scala programming language. CafeSat is a modern solver based on DPLL and featuring many state-of-the-art techniques and heuristics. It uses two-watched literals for Boolean constraint propagation, conflict-dr ...

ACM Press2013