Author name cluster

Norbert Manthey

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

1 author row

SAT Conference 2021 Conference Paper

The MergeSat Solver

Norbert Manthey

Abstract 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. Furthermore, bug fixes in one solver do not evolve into predecessors. This work presents MergeSat, a SAT solver that is also based on leading solvers of the past years. However, MergeSat can replace MiniSat or Glucose, as relevant features have been added back. Also, new techniques from other solvers of the community have been adapted, and implementation issues have been identified and fixed. These issues did not surface in an original solver or its successor during competitions. Finally, we provide a mechanism to easily incorporate changes of other solver, as well as a development and test environment to identify potential issues when merging techniques early. With this setup, MergeSat is a good starting point for future research development and integration into other solvers.

Details

SAT Conference 2016 Conference Paper

BEACON: An Efficient SAT-Based Tool for Debugging EL ^+ Ontologies

M. Fareed Arif
Carlos Mencía
Alexey Ignatiev
Norbert Manthey
Rafael Peñaloza
João Marques-Silva 0001

Abstract Description Logics (DLs) are knowledge representation and reasoning formalisms used in many settings. Among them, the \({\mathcal {EL}}\) family of DLs stands out due to the availability of polynomial-time inference algorithms and its ability to represent knowledge from domains such as medical informatics. However, the construction of an ontology is an error-prone process which often leads to unintended inferences. This paper presents the BEACON tool for debugging \({\mathcal {EL}{^+}}\) ontologies. BEACON builds on earlier work relating minimal justifications (MinAs) of \({\mathcal {EL}{^+}}\) ontologies and MUSes of a Horn formula, and integrates state-of-the-art algorithms for solving different function problems in the SAT domain.

Details

SAT Conference 2016 Conference Paper

SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers

Norbert Manthey
Marius Lindauer

Abstract Automated configuration is used to improve the performance of a SAT solver. Increasing the space of possible parameter configurations leverages the power of configuration but also leads to harder maintainable code and to more undiscovered bugs. We present the tool SpyBug that finds erroneous minimal parameter configurations of SAT solvers and their parameter specification to help developers to identify and narrow down bugs in their solvers. The importance of SpyBug is shown by the bugs we found for four well-known SAT solvers that won prices in international competitions.

Details

SAT Conference 2015 Conference Paper

Recognition of Nested Gates in CNF Formulas

Ashlin Iser
Norbert Manthey
Carsten Sinz

Abstract We present a new algorithm to efficiently extract information about nested functional dependencies between variables of a formula in CNF. Our algorithm uses the relation between gate encodings and blocked sets in CNF formulas. Our notion of “gate” emphasizes this relation. The presented algorithm is central to our new tool, cnf2aig, that produces equisatisfiable and-inverter-graphs (AIGs) from CNF formulas. We compare the novel algorithm to earlier approaches and show that the produced AIG are generally more succinct and use less input variables. As the gate-detection is related to the structure of input formulas, we furthermore analyze the gate-detection before and after applying preprocessing techniques.

Details

SAT Conference 2014 Conference Paper

Detecting Cardinality Constraints in CNF

Armin Biere
Daniel Le Berre
Emmanuel Lonca
Norbert Manthey

Abstract We present novel approaches to detect cardinality constraints expressed in CNF. The first approach is based on a syntactic analysis of specific data structures used in SAT solvers to represent binary and ternary clauses, whereas the second approach is based on a semantic analysis by unit propagation. The syntactic approach computes an approximation of the cardinality constraints AtMost-1 and AtMost-2 constraints very fast, whereas the semantic approach has the property to be generic, i. e. it can detect cardinality constraints AtMost- k for any k, at a higher computation cost. Our experimental results suggest that both approaches are efficient at recovering AtMost-1 and AtMost-2 cardinality constraints.

Details

SAT Conference 2013 Conference Paper

Parallel MUS Extraction

Anton Belov
Norbert Manthey
João Marques-Silva 0001

Abstract Parallelization is a natural direction towards the improvements in the scalability of algorithms for the computation of Minimally Unsatisfiable Subformulas (MUSes), and group-MUSes, of CNF formulas. In this paper we propose and analyze a number of approaches to parallel MUS computation. Just as it is the case with the parallel CDCL-based SAT solving, the communication, i. e. the exchange of learned clauses between the solvers running in parallel, emerges as an important component of parallel MUS extraction algorithms. However, in the context of MUS computation the communication might be unsound. We argue that the assumption-based approach to the incremental CDCL-based SAT solving is the key enabling technology for effective sound communication in the context of parallel MUS extraction, and show that fully unrestricted communication is possible in this setting. Furthermore, we propose a number of techniques to improve the quality of communication, as well as the quality of job distribution in the parallel MUS extractor. We evaluate the proposed techniques empirically on industrially-relevant instances of both plain and group MUS problems, and demonstrate significant (up to an order of magnitude) improvements due to the parallelization.

Details

SAT Conference 2013 Conference Paper

Soundness of Inprocessing in Clause Sharing SAT Solvers

Norbert Manthey
Tobias Philipp
Christoph Wernhard

Abstract We present a formalism that models the computation of clause sharing portfolio solvers with inprocessing. The soundness of these solvers is not a straightforward property since shared clauses can make a formula unsatisfiable. Therefore, we develop characterizations of simplification techniques and suggest various settings how clause sharing and inprocessing can be combined. Our formalization models most of the recent implemented portfolio systems and we indicate possibilities to improve these. A particular improvement is a novel way to combine clause addition techniques – like blocked clause addition – with clause deletion techniques – like blocked clause elimination or variable elimination.

Details

SAT Conference 2012 Conference Paper

Coprocessor 2. 0 - A Flexible CNF Simplifier - (Tool Presentation)

Norbert Manthey

Abstract This paper presents the CNF simplifier Coprocessor 2. 0, an extension of Coprocessor [1]. It implements almost all currently known simplification techniques in a modular way and provides access to each single technique to execute them independently. Disabling preprocessing for a set of variables is also possible and enables to apply simplifications also for incremental SAT solving. Experiments show that Coprocessor 2. 0 performs better than its predecessor or SatElite [2].

Details

SAT Conference 2012 Conference Paper

Designing Scalable Parallel SAT Solvers

Antti E. J. Hyvärinen
Norbert Manthey

Abstract Solving instances of the propositional satisfiability problem (SAT) in parallel has received a significant amount of attention as the number of cores in a typical workstation is steadily increasing. With the increase of the number of cores, in particular the scalability of such approaches becomes essential for fully harnessing the potential of modern architectures. The best parallel SAT solvers have, until recently, been based on algorithm portfolios, while search-space partitioning approaches have been less successful. We prove, under certain natural assumptions on the partitioning function, that search-space partitioning can always result in an increased expected run time, justifying the success of the portfolio approaches. Furthermore, we give first controlled experiments showing that an approach combining elements from partitioning and portfolios scales better than either of the two approaches and succeeds in solving instances not solved in a recent solver competition.

Details