Semantisches Browsen
Aus International Center for Computational Logic
This thesis focuses on improving the SAT s … This thesis focuses on improving the SAT solving technology. The improvements focus on two major subjects: sequential SAT solving and parallel SAT solving.</br></br>To better understand sequential SAT algorithms, the abstract reduction system Generic CDCL is introduced. With Generic CDCL, the soundness of solving techniques can be modeled. Next, the conflict driven clause learning algorithm is extended with the three techniques local look-ahead, local probing and all UIP learning that allow more global reasoning during search. These techniques improve the performance of the sequential SAT solver Riss. Then, the formula simplification techniques bounded variable addition, covered literal elimination and an advanced cardinality constraint extraction are introduced. By using these techniques, the reasoning of the overall SAT solving tool chain becomes stronger than plain resolution. When using these three techniques in the formula simplification tool Coprocessor before using Riss to solve a formula, the performance can be improved further.</br></br>Due to the increasing number of cores in CPUs, the scalable parallel SAT solving approach iterative partitioning has been implemented in Pcasso for the multi-core architecture. Related work on parallel SAT solving has been studied to extract main ideas that can improve Pcasso. Besides parallel formula simplification with bounded variable elimination, the major extension is the extended clause sharing level based clause tagging, which builds the basis for conflict driven node killing. The latter allows to better identify unsatisfiable search space partitions. Another improvement is to combine scattering and look-ahead as a superior search space partitioning function. In combination with Coprocessor, the introduced extensions increase the performance of the parallel solver Pcasso. The implemented system turns out to be scalable for the multi-core architecture. Hence iterative partitioning is interesting for future parallel SAT solvers.</br></br>The implemented solvers participated in international SAT competitions. In 2013 and 2014 Pcasso showed a good performance. Riss in combination with Copro- cessor won several first, second and third prices, including two Kurt-Gödel-Medals. Hence, the introduced algorithms improved modern SAT solving technology.ms improved modern SAT solving technology.
@phdthesis{M2014,
author = {Norbert Manthey},
title = {Towards Next Generation Sequential and Parallel {SAT} Solvers},
school = {TU Dresden},
year = {2014}
}
author = {Norbert Manthey},
title = {Towards Next Generation Sequential and Parallel {SAT} Solvers},
school = {TU Dresden},
year = {2014}
}
Date"Date" is a <a href="/web/Spezial:Datentypen/Date" title="Spezial:Datentypen/Date">type</a> and predefined property provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> to represent date values.
1. Dezember 2014 +
Manthey +
Norbert +
Norbert Manthey<br /> '''[[Phdthesis3002|Towards Next Generation Sequential and Parallel SAT Solvers]] … Norbert Manthey<br /> '''[[Phdthesis3002|Towards Next Generation Sequential and Parallel SAT Solvers]]''' <br>__NOTOC__Phd thesis, TU Dresden, 2014/12/01<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Phdthesis3002|Details]]Phdthesis3002|Details]] +
Norbert Manthey <br /> '''[[Phdthesis3002/en|Towards Next Generation Sequential and Parallel SAT Solvers]] … Norbert Manthey <br /> '''[[Phdthesis3002/en|Towards Next Generation Sequential and Parallel SAT Solvers]]''' <br>__NOTOC__Phd thesis, TU Dresden, 2014/12/01<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Phdthesis3002|Details]]Phdthesis3002|Details]] +
Display title of"Display title of" is a predefined property that can assign a distinct display title to an entity and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
Towards Next Generation Sequential and Parallel SAT Solvers +
Modification date"Zuletzt geändert <span style="font-size:small;">(Modification date)</span>" is a predefined property that corresponds to the date of the last modification of a subject and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
15. Januar 2015, 09:23:10 +
Has query"Hat Abfrage <span style="font-size:small;">(Has query)</span>" is a predefined property that represents meta information (in form of a <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">subobject</a>) about individual queries and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
Towards Next Generation Sequential and Parallel SAT Solvers +, Towards Next Generation Sequential and Parallel SAT Solvers +, Towards Next Generation Sequential and Parallel SAT Solvers +, Towards Next Generation Sequential and Parallel SAT Solvers + and Towards Next Generation Sequential and Parallel SAT Solvers +
