Publication

Decision Procedures for Multisets with Cardinality Constraints

Related publications (78)

Decision Procedures for Power Structures

We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction ...

EPFL2023

Simulating intra-household interactions for in- and out-of-home activity scheduling

Michel Bierlaire, Timothy Michael Hillel, Negar Rezvany

Various interactions, time arrangements, and constraints exist for individuals scheduling their day as a member of a household, which affect their in-home as well as out-of-home activity schedule. However, the existing activity-based models are mostly base ...

Oxford2023

Simulating intra-household interactions for in- and out-of-home activity scheduling

Michel Bierlaire, Timothy Michael Hillel, Negar Rezvany

2023

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

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

We consider various versions of the obstacle and thin-obstacle problems, we interpret them as variational inequalities, with non-smooth constraint, and prove that they satisfy a new constrained Lojasiewicz inequality. The difficulty lies in the fact that, ...

2020

We introduce a novel approach to reduce the computational effort of solving convex chance constrained programs through the scenario approach. Instead of reducing the number of required scenarios, we directly minimize the computational cost of the scenario ...

2019

Designing Coalition-Proof Reverse Auctions Over Continuous Goods

Maryam Kamgarpour, Orcun Karaca

This paper investigates reverse auctions that involve continuous values of different types of goods, general nonconvex constraints, and second stage costs. We seek to design the payment rules and conditions under which coalitions of participants cannot inf ...

2019

Refutation-based synthesis in SMT

Viktor Kuncak, Andrew Joseph Reynolds

We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...

SPRINGER2019

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

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.