Concept

Problème SAT

Publications associées (124)

Strong LP Formulations for Scheduling Splittable Jobs on Unrelated Machines

We study a natural generalization of the problem of minimizing makespan on unrelated machines in which jobs may be split into parts. The different parts of a job can be (simultaneously) processed on different machines, but each part requires a setup time b ...

Springer2014

An online-offline homogenization strategy to solve quasilinear two-scale problems at the cost of one-scale problems

Assyr Abdulle, Gilles Vilmart, Yun Bai

Inspired by recent analyses of the finite element heterogeneous multiscale method and the reduced basis technique for nonlinear problems, we present a simple and concise finite element algorithm for the reliable and efficient resolution of elliptic or para ...

Wiley-Blackwell2014

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

Computing with an SMT Solver

Tiark Rompf, Nada Amin

Satisfiability modulo theories (SMT) solvers that support quantifier instantiations via matching triggers can be programmed to give practical support for user-defined theories. Care must be taken to avoid so-called matching loops, which may prevent termina ...

2014

CafeSat: a Modern SAT Solver for Scala

Régis William Blanc

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

On Cafesat: A Modern SAT Solver for Scala

Régis William Blanc

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

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

MPTCP Is Not Pareto-Optimal: Performance Issues and a Possible Solution

Jean-Yves Le Boudec, Nicolas Gabriel Gast, Ramin Khalili, Miroslav Popovic

Multipath TCP (MPTCP) has been proposed recently as a mechanism for transparently supporting multiple connections to the application layer. It is under discussion at the IETF. We nevertheless demonstrate that the current MPTCP suffers from two problems: P1 ...

Ieee-Inst Electrical Electronics Engineers Inc2013

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

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search