Publications related to 2-satisfiability

On Semi-Algebraic Proofs and Algorithms

We give a new characterization of the Sherali-Adams proof system, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula C if and only if there is an ε > 0 and a degree-d conical junta J such that viol_C(x) - ε = J, where ...

Schloss Dagstuhl - Leibniz-Zentrum für Informatik2022

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

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

Springer, Cham2022

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

Raffaele Marino

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

IOP PUBLISHING LTD2021

Boolean satisfiability in quantum compilation

Giovanni De Micheli, Mathias Soeken, Fereshte Mozafari Ghoraba, Heinz Riener, Giulia Meuli, Bruno Schmitt Antunes

Quantum compilation is the task of translating a quantum algorithm implemented in a high-level quantum programming language into a technology-dependent instructions flow for a physical quantum computer. To tackle the large gap between the quantum program a ...

ROYAL SOC2020

Symbolic Algorithms for Token Swapping

Giovanni De Micheli, Mathias Soeken, Bruno Schmitt Antunes

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

2020

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

Giovanni De Micheli, Mathias Soeken, Winston Jason Haaswijk, Zhufei Chu

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

IEEE2019

SAT-Based Exact Synthesis for Multi-Level Logic Networks

Winston Jason Haaswijk

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

EPFL2019

Canonical Computation without Canonical Representation

Mathias Soeken, Luca Gaetano Amarù, Ana Petkovska

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

IEEE2018

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

Andrew James Becker

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

EPFL2018

SAT-Based Area Recovery in Structural Technology Mapping

Bruno Schmitt Antunes

This paper proposes a fast SAT-based algorithm for recovering area applicable to an already technology mapped circuit. The algorithm considers a sequence of relatively small overlapping regions, called windows, in a mapped network and tries to improve the ...

ASSOC COMPUTING MACHINERY2018

Practical Exact Synthesis

Giovanni De Micheli, Mathias Soeken, Luca Gaetano Amarù, Eleonora Testa, Winston Jason Haaswijk

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

IEEE2018

Busy Man’s Synthesis: Combinational Delay Optimization With SAT

Giovanni De Micheli, Mathias Soeken

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

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

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

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

Method for speeding up boolean satisfiability

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

A method for transforming a tautology check of an original logic circuit into a contradiction check of the original logic circuit and vice versa comprises interpreting the original logic circuit in terms of AND, OR, MAJ, MIN, XOR, XNOR, INV original logic ...

2016

Exploiting Circuit Duality to Speed Up SAT

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù, Maciej Jerzy Ciesielski

In this paper, we establish a non-trivial duality between tautology and contradiction check to speed up circuit SAT. Tautology check determines if a logic circuit is true in every possible interpretation. Analogously, contradiction check dete ...

IEEE2015

Majority Logic Representation and Satisfiability

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

Majority logic is a powerful generalization of common AND/OR logic. Original two-level and multi-level logic networks can use majority operators as primitive connective, in place of AND/ORs. In such a way, Boolean functions have novel means for compact rep ...

2014

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

Outsourced Pattern Matching

Sebastian Faust

In secure delegatable computation, computationally weak devices (or clients) wish to outsource their computation and data to an untrusted server in the cloud. While most earlier work considers the general question of how to securely outsource any computati ...

2013