Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Maximum satisfiability problem

Publications associées (13)

Approximation Algorithms for Allocation and Network Design

Etienne Michel François Bamas

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

EPFL2023

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, Heinz Riener, Bruno Schmitt Antunes, Giulia Meuli, Fereshte Mozafari Ghoraba

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

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

Optimal Software Patching Plan for PMUs

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

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

A Sound and Complete Axiomatization of Majority-n Logic

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

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

Decomposition and tractability in qualitative spatial and temporal reasoning

Jingshi Li

Constraint networks in qualitative spatial and temporal reasoning (QSTR) typically feature variables defined on infinite domains. Mainstream algorithms for deciding network consistency are based on searching for network refinements whose consistency is kno ...

Elsevier2013

An overview of the Leon verification system: verification by translation to recursive functions

Viktor Kuncak, Philippe Paul Henri Suter, Régis William Blanc, Etienne Kneuss

We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Bo ...

2013

Santa Claus Schedules Jobs On Unrelated Machines

Ola Nils Anders Svensson

One of the classic results in scheduling theory is the 2-approximation algorithm by Lenstra, Shmoys, and Tardos for the problem of scheduling jobs to minimize makespan on unrelated machines; i.e., job j requires time p(ij) if processed on machine i. More t ...

Siam Publications2012

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Pricing on Paths: A PTAS for the Highway Problem

Thomas Rothvoss

In the highway problem, we are given an n-edge line graph (the highway), and a set of paths (the drivers), each one with its own budget. For a given assignment of edge weights (the tolls), the highway owner collects from each driver the weight of the assoc ...

2011

Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We consider an extension of integer linear arithmetic with a “star” operator takes closure under vector addition of the solution set of a linear arithmetic subformula. We show that the satisfiability problem for this extended language remains in NP (and th ...

Springer2008