Planning with Learned Binarized Neural Networks Benchmarks for MaxSAT Evaluation 2021

Autor: Say, Buser, Sanner, Scott, Devriendt, Jo, Nordström, Jakob, Stuckey, Peter J.

This document provides a brief introduction to learned automated planning problem where the state transition function is in the form of a binarized neural network (BNN), presents a general MaxSAT encoding for this problem, and describes the four doma

Externí odkaz: http://arxiv.org/abs/2108.00633

BreakID: Static Symmetry Breaking for ASP (System Description)

Autor: Devriendt, Jo, Bogaerts, Bart

Symmetry breaking has been proven to be an efficient preprocessing technique for satisfiability solving (SAT). In this paper, we port the state-of-the-art SAT symmetry breaker BreakID to answer set programming (ASP). The result is a lightweight tool

Externí odkaz: http://arxiv.org/abs/1608.08447

On Local Domain Symmetry for Model Expansion

Autor: Devriendt, Jo, Bogaerts, Bart, Bruynooghe, Maurice, Denecker, Marc

Symmetry in combinatorial problems is an extensively studied topic. We continue this research in the context of model expansion problems, with the aim of automating the workflow of detecting and breaking symmetry. We focus on local domain symmetry, w

Externí odkaz: http://arxiv.org/abs/1608.02688

Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning

Autor: Liew, Vincent, Beame, Paul, Devriendt, Jo, Elffers, Jan, Nordström, Jakob

Publikováno v: Liew, V, Beame, P, Devriendt, J, Elffers, J & Nordström, J 2020, Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning . in Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design (FMCAD '20) ., 9283622, IEEE, pp. 194-204, 20th International Conference on Formal Methods in Computer-Aided Design-FMCAD 2020;, Virtual, 21/09/2020 . https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_27

Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SAT-based bit-vector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is in

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______2751::530ade98461ededd5792959acc6fb2a8
https://curis.ku.dk/portal/da/publications/verifying-properties-of-bitvector-multiplication-using-cutting-planes-reasoning(d08d12c1-8aad-4d9e-9cc1-52679e7c5673).html

Exploiting Symmetry in Model Expansion for Predicate and Propositional Logic : Symmetrie uitbuiten in modelexpansie voor predikaten- en propositionele logica

Autor: Devriendt, Jo

Many combinatorial problems exhibit symmetry, a transformational property that does not fundamentally alter the nature of a problem. For instance, renaming a set of identical trucks in a routing problem, mirroring or rotating a chessboard onto itself

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______1131::ca17baebc28709f41f823c006bb5eeff
https://lirias.kuleuven.be/handle/123456789/564687