Publication

NP Satisfiability for Arrays as Powers

Publications associées (28)

Busy Man’s Synthesis: Combinational Delay Optimization With SAT

Boolean SAT solving can be used to find a minimum- size logic network for a given small Boolean function. This paper extends the SAT formulation to find a minimum-size network under delay constraints. Delay constraints are given in terms of input arrival t ...

Ieee2017

Solving quantified linear arithmetic by counterexample-guided instantiation

Viktor Kuncak, Andrew Joseph Reynolds

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...

2017

Exact Synthesis of Majority-Inverter Graphs and Its Applications

Giovanni De Micheli, Luca Gaetano Amarù, Pierre-Emmanuel Julien Marc Gaillardon, Mathias Soeken

We propose effective algorithms for exact synthesis of Boolean logic networks using satisfiability modulo theories (SMT) solvers. Since exact synthesis is a difficult problem, it can only be applied efficiently to very small functions, having up to 6 varia ...

Ieee-Inst Electrical Electronics Engineers Inc2017

Exploiting Satisfiability Solvers for Efficient Logic Synthesis

Ana Petkovska

Logic synthesis is an important part of electronic design automation (EDA) flows, which enable the implementation of digital systems. As the design size and complexity increase, the data structures and algorithms for logic synthesis must adapt and improve ...

EPFL2017

Optimal Software Patching Plan for PMUs

Jean-Yves Le Boudec, Teklemariam Tsegay Tesfay, Ola Nils Anders Svensson

Phasor measurement units (PMUs) deployed to monitor the state of an electrical grid need to be patched from time to time to prevent attacks that exploit vulnerabilities in the software. Applying some of these patches requires a PMU reboot, which takes the ...

2017

Proactive Synthesis of Recursive Tree-to-String Functions from Examples

Viktor Kuncak, Mikaël Mayer, Jad Hamza

Synthesis from examples enables non-expert users to generate programs by specifying examples of their behavior. A domain-specific form of such synthesis has been recently deployed in a widely used spreadsheet software product. In this paper we contribute t ...

2017

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

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

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

A Sound and Complete Axiomatization of Majority-n Logic

Giovanni De Micheli, Luca Gaetano Amarù, Pierre-Emmanuel Julien Marc Gaillardon, 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