Publication

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

Related publications (27)

Orthologic with Axioms

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

Fairness and Explainability in Clustering Problems

Xinrui Jia

In this thesis we present and analyze approximation algorithms for three different clustering problems. The formulations of these problems are motivated by fairness and explainability considerations, two issues that have recently received attention in the ...

EPFL2023

Learning Sparse Graphons And The Generalized Kesten-Stigum Threshold

Emmanuel Abbé

The problem of learning graphons has attracted considerable attention across several scientific communities, with significant progress over the re-cent years in sparser regimes. Yet, the current techniques still require diverg-ing degrees in order to succe ...

INST MATHEMATICAL STATISTICS-IMS2023

How to Find Molecules with Long-lasting Charge Migration?

Jiri Vanicek, Alan Scheidegger, Nikolay Golubev

Under certain conditions, the ionization of a molecule may create a superposition of electronic states, leading to ultrafast electron dynamics. If controlled, this motion could be used in attochemistry applications, but it has been shown that the decoheren ...

SWISS CHEMICAL SOC2023

Sketches, metrics and fast algorithms

Navid Nouri

As it has become easier and cheaper to collect big datasets in the last few decades, designing efficient and low-cost algorithms for these datasets has attracted unprecedented attention. However, in most applications, even storing datasets as acquired has ...

EPFL2022

Sequential metric dimension for random graphs

Patrick Thiran, Gergely Odor

In the localization game on a graph, the goal is to find a fixed but unknown target node v* with the least number of distance queries possible. In the j-th step of the game, the player queries a single node v_j and receives, as an answer to their query, th ...

2021

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

Association for Computing Machinery2024

Fairness and Explainability in Clustering Problems

Xinrui Jia

EPFL2023

Learning Sparse Graphons And The Generalized Kesten-Stigum Threshold

Emmanuel Abbé

INST MATHEMATICAL STATISTICS-IMS2023

How to Find Molecules with Long-lasting Charge Migration?

Jiri Vanicek, Alan Scheidegger, Nikolay Golubev

SWISS CHEMICAL SOC2023

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

Sketches, metrics and fast algorithms

Navid Nouri

EPFL2022

Metric dimension of critical Galton–Watson trees and linear preferential attachment trees

Gergely Odor

The metric dimension of a graph G is the minimal size of a subset R of vertices of G that, upon reporting their graph distance from a distinguished (source) vertex v⋆, enable unique identification of the source vertex v⋆ among all possible vertices of G. I ...

2021

Sequential metric dimension for random graphs

Patrick Thiran, Gergely Odor

2021

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