Zobrazeno 1 - 10
of 27
pro vyhledávání: '"Norbert Manthey"'
Autor:
Norbert Manthey
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2021 ISBN: 9783030802226
SAT
SAT
Successful SAT solvers in recent competitions are typically based on the winner of the previous competition. Due to this procedure, for multiple years relevant features like incremental solving have not been supported by winning solvers anymore. Furt
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c01ee865473a6ab3ee6c532d5ccc0df7
https://doi.org/10.1007/978-3-030-80223-3_27
https://doi.org/10.1007/978-3-030-80223-3_27
Publikováno v:
KI-Künstliche Intelligenz
One approach to axiom pinpointing (AP) in description logics is its reduction to the enumeration of minimal unsatisfiable subformulas, allowing for the deployment of highly optimized methods from SAT solving. Exploiting the properties of AP, we furth
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::68df89c84e1db289c8e3ff77fd046590
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030584740
CP
CP
Various state-of-the-art automated reasoning (AR) tools are widely used as backend tools in research of knowledge representation and reasoning as well as in industrial applications. In testing and verification, those tools often run continuously or n
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c20d9a88f247a1e7389b2c3b6ff4b920
https://doi.org/10.1007/978-3-030-58475-7_18
https://doi.org/10.1007/978-3-030-58475-7_18
Autor:
Norbert Manthey, Tobias Philipp
Publikováno v:
POS@SAT
Contemporary SAT solvers emit unsatisfiability proofs in the DRAT format to increase confidence in their answers. The state-of-the-art proof verifier drat-trim uses backward- checking and deletion information to efficiently check unsatisfiability res
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a81e494790a64a3dfa60f6387e83f7db
https://doi.org/10.29007/8w4v
https://doi.org/10.29007/8w4v
Publikováno v:
POS@SAT
As satisfiability (SAT) solver performance has improved, so has their complexity, which make it more likely that SAT solvers contain bugs. One important source of increased complexity is clause sharing in parallel SAT solvers. SAT solvers can emit a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2e0224b100039c7fb15f691b0fa97c6e
https://doi.org/10.29007/6vwg
https://doi.org/10.29007/6vwg
Publikováno v:
EPiC Series in Computing.
Nowadays, powerful parallel SAT solvers are based on an algorithm portfolio. Thealternative approach, (iterative) search space partitioning, cannot keep up, although, ac-cording to the literature, iterative partitioning systems should scale better th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4d70c36878ad3da76f10f290c5b2cc10
https://doi.org/10.29007/jnvf
https://doi.org/10.29007/jnvf
Autor:
Norbert Manthey, Ari Saptawijaya
Publikováno v:
EPiC Series in Computing.
The paper presents our work on cache analysis of SAT-solving. The aim is to study how resources are utilized by a SAT-solver and to use this knowledge to improve the resource usage in SAT-solving. The analysis is performed mainly on our CDCL-based SA
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cae8b0bf96e91d42aa1a70556c3e235e
https://doi.org/10.29007/3vwv
https://doi.org/10.29007/3vwv
Autor:
Adrian Balint, Norbert Manthey
Publikováno v:
POS@SAT
Preprocessing techniques are crucial for SAT solvers when it comes to reaching state-of-the-art performance as it was shown by the results of the last SAT Competitions. Theusefulness of a preprocessing technique depends highly on its own parameters,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7c103828055dd1280ffa07012124de18
https://doi.org/10.29007/28ww
https://doi.org/10.29007/28ww
Publikováno v:
POS@SAT
Modern propositional satisfiability (or SAT) solvers are very powerful due to recent developments on the underlying data structures, the used heuristics to guide the search, the deduction techniques to infer knowledge, and the formula simplification
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f28881c63a568710e2076a61c4efead1
https://doi.org/10.29007/7n71
https://doi.org/10.29007/7n71
Autor:
Enrique Matos Alfonso, Norbert Manthey
Publikováno v:
POS@SAT
In this paper we first present three new features for classifying CNF formulas. These features are based on the structural information of the formula and consider AND-gates as well as exactly-one constraints. Next, we use these features to construct
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::fb78ef78048038003e6843fdcec665c4
https://doi.org/10.29007/b8t1
https://doi.org/10.29007/b8t1