Concept

Horn-satisfiability

Related publications (33)

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.

SATSoT: A Methodology to Map Controllable-Polarity Devices on a Regular Fabric Using SAT

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Catherine Lucie Jéromine Gasnier

Devices with controllable-polarity, such as Double-Gate Vertically-Stacked Nanowire FETs, have shown promising interests in recent years to implement XOR-based logic functions in an unprecedented compact way. Such a compactness is obtained at the cost of a ...

2013

Polarization and Spatial Coupling

Seyed Hamed Hassani

During the last two decades we have witnessed considerable activity in building bridges between the fields of information theory/communications, computer science, and statistical physics. This is due to the realization that many fundamental concepts and no ...

EPFL2013

Satisfiability Modulo Recursive Programs

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of expressive correctness properties of recursive first-order functional programs. In our approach, both properties and programs are expressed in the same language, a subset of Scala. We impl ...

Springer-Verlag Berlin2011

Scala to the Power of Z3: Integrating SMT and Programming

Viktor Kuncak, Philippe Paul Henri Suter

We describe a system that integrates the SMT solver Z3 with the Scala programming language. The system supports the use of the SMT solver for checking satisfiability, unsatisfiability, as well as solution enumeration. The embedding of formula trees into Sc ...

Springer-Verlag Berlin2011

Verification of consensus algorithms using satisfiability solving

André Schiper

Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms ...

Springer Verlag2011

On Deciding Functional Lists with Sublist Sets

Viktor Kuncak

Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for lo ...

2010

On Satisfiability Modulo Computable Functions

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...

2010

On Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas ...

2009

Functional dependencies in OWL ABoxes

Jean Paul Calbimonte Perez

Functional Dependency (FD) has been extensively studied in database theory. Most recently there have been some works investigating the implications of extending Description Logics with functional dependencies. In particular the OWL ontology language offers ...

2009

Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We present decision procedures for logical constraints that support reasoning about collections of elements such as sets, multisets, and fuzzy sets. Element membership in such collections is given by a characteristic function from a finite universe (of unk ...

2008