Výsledky vyhledávání - "Alexander Nadel"

Local Search with a SAT Oracle for Combinatorial Optimization

Autor: Vadim Ryvchin, Alexander Nadel, Aviad Cohen

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030720124
TACAS (2)

NP-hard combinatorial optimization problems are pivotal in science and business. There exists a variety of approaches for solving such problems, but for problems with complex constraints and objective functions, local search algorithms scale the best

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::e1a6ee7d685e8cd62a016b6593a4075a
https://doi.org/10.1007/978-3-030-72013-1_5

Zobrazit plný text záznamu

Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization

Autor: Alexander Nadel

Publikováno v: FMCAD

This paper introduces a new anytime algorithm for Weighted MaxSAT consisting of two main algorithmic components. First, we propose a new efficient polarity selection heuristic and an enhancement to the variable decision heuristic for SAT-based anytim

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::5793b17a6527fbe8b89daabbf52d96bc
https://doi.org/10.23919/fmcad.2019.8894273

Zobrazit plný text záznamu

Efficient generation of small interpolants in CNF

Autor: Vadim Ryvchin, Alexander Nadel, Yakir Vizel

Publikováno v: Formal Methods in System Design. 47:51-74

Interpolation-based model checking (ITP) McMillan (in CAV, 2003) is an efficient and complete model checking procedure. However, for large problems, interpolants generated by ITP might become extremely large, rendering the procedure slow or even intr

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::4f6038ef0becc5d718ec47b27b79a62e
https://doi.org/10.1007/s10703-015-0224-5

Zobrazit plný text záznamu

Solving MaxSAT with Bit-Vector Optimization

Autor: Alexander Nadel

Publikováno v: Theory and Applications of Satisfiability Testing – SAT 2018 ISBN: 9783319941431
SAT

We explore the relationships between two closely related optimization problems: MaxSAT and Optimization Modulo Bit-Vectors (OBV). Given a bit-vector or a propositional formula F and a target bit-vector T, Unweighted Partial MaxSAT maximizes the numbe

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::59a4c5eba411428219743acdf391cd64
https://doi.org/10.1007/978-3-319-94144-8_4

Zobrazit plný text záznamu

Chronological Backtracking

Autor: Alexander Nadel, Vadim Ryvchin

Publikováno v: Theory and Applications of Satisfiability Testing – SAT 2018 ISBN: 9783319941431

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::4f5c215c009843a921dcd2b08ff7e536
https://doi.org/10.1007/978-3-319-94144-8_7

Zobrazit plný text záznamu

Solving linear arithmetic with SAT-based model checking

Autor: Yakir Vizel, Alexander Nadel, Sharad Malik

Publikováno v: FMCAD

We present LIAMC, a novel decision procedure for (quantifier-free) linear arithmetic over both integers modulo 2N (LIA n ) and integers (LIA). There is no need to explain our motivation to design a new efficient decision procedure for the widely used

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::116cab51cd645a5c45e2c8e65cc17ee3
https://doi.org/10.23919/fmcad.2017.8102240

Zobrazit plný text záznamu

Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores

Autor: Vadim Ryvchin, Alexander Nadel, Ofer Strichman

Publikováno v: Journal on Satisfiability, Boolean Modeling and Computation. 9:27-51

Various technologies are based on the capability to find small unsatisfiable cores given an unsatisfiable CNF formula, i.e., a subset of the clauses that are unsatisfiable regardless of the rest of the formula. If that subset is irreducible, it is ca

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::a2d3da9b4273162f5c0cf287dca3b384
https://doi.org/10.3233/sat190100

Zobrazit plný text záznamu

A Correct-by-Decision Solution for Simultaneous Place and Route

Autor: Alexander Nadel

Publikováno v: Computer Aided Verification ISBN: 9783319633893
CAV (2)

To reduce a problem, provided in a human language, to constraint solving, one normally maps it to a set of constraints, written in the language of a suitable logic. This paper highlights a different paradigm, in which the original problem is converte

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::8ec78336c400ab71f3adfea5487bc8d7
https://doi.org/10.1007/978-3-319-63390-9_23

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání