Semantisches Browsen
Aus International Center for Computational Logic
Inprocessing is to apply clause simplifica … Inprocessing is to apply clause simplification techniques during search and is a very attractive idea since it allows to apply computationally expensive techniques. In this paper we present the search space decomposition formalism SSD that models parallel SAT solvers with clause sharing and inprocessing. The main result of this paper is that the sharing model SSD is sound. In the formalism, we combine clause addition and clause elimination techniques, and it covers many SAT solvers such as PaSAT, PaMira, PMSat, MiraXT and ccc. Inprocessing is not used in these solvers, and we therefore propose a novel way how to combine clause sharing, search space decomposition and inprocessing.arch space decomposition and inprocessing. +
@inproceedings{P2014,
author = {Tobias Philipp},
title = {Clause Simplifications in Search-Space Decomposition-Based {SAT}
Solvers},
editor = {Ulle Endriss and Jo{\~{a}}o Leite},
booktitle = {7th European Starting {AI} Researcher Symposium (STAIRS)},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {264},
publisher = {IOS Press},
year = {2014},
pages = {211-219}
}
author = {Tobias Philipp},
title = {Clause Simplifications in Search-Space Decomposition-Based {SAT}
Solvers},
editor = {Ulle Endriss and Jo{\~{a}}o Leite},
booktitle = {7th European Starting {AI} Researcher Symposium (STAIRS)},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {264},
publisher = {IOS Press},
year = {2014},
pages = {211-219}
}
Philipp +
Tobias +
Tobias Philipp<br/> '''[[Article3011|<b>Clause Simplifications in Search-Space Decomposition-Based SAT Solvers</b>]] … Tobias Philipp<br/> '''[[Article3011|<b>Clause Simplifications in Search-Space Decomposition-Based SAT Solvers</b>]]''' <br/>__NOTOC__In Ulle Endriss, João Leite, eds., <i>7th European Starting AI Researcher Symposium (STAIRS)</i>, volume 264 of Frontiers in Artificial Intelligence and Applications, 211-219, 2014. IOS Press<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Article3011|Details]]011|Details]] +
Tobias Philipp<br/> '''[[Article3011/en|<b>Clause Simplifications in Search-Space Decomposition-Based SAT Solvers</b>]] … Tobias Philipp<br/> '''[[Article3011/en|<b>Clause Simplifications in Search-Space Decomposition-Based SAT Solvers</b>]]''' <br/>__NOTOC__In Ulle Endriss, João Leite, eds., <i>7th European Starting AI Researcher Symposium (STAIRS)</i>, volume 264 of Frontiers in Artificial Intelligence and Applications, 211-219, 2014. IOS Press<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Article3011|Details]]011|Details]] +
Anzeigetitel„Anzeigetitel <span style="font-size:small;">(Display title of)</span>“ ist ein softwareseitig fest definiertes Attribut, das einen eindeutigen Anzeigetitel zu einem Objekt speichert und ihm zuweist. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Clause Simplifications in Search-Space Decomposition-Based SAT Solvers +
Zuletzt geändert„Zuletzt geändert <span style="font-size:small;">(Modification date)</span>“ ist ein softwareseitig fest definiertes Attribut, das das Datum der letzten Änderung einer Seite speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
11. Juni 2015, 12:26:27 +
Hat Abfrage„Hat Abfrage <span style="font-size:small;">(Has query)</span>“ ist ein softwareseitig fest definiertes Attribut, das die Metainformationen einer Abfrage als <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">Subobjekt</a> speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Clause Simplifications in Search-Space Decomposition-Based SAT Solvers +, Clause Simplifications in Search-Space Decomposition-Based SAT Solvers +, Clause Simplifications in Search-Space Decomposition-Based SAT Solvers +, Clause Simplifications in Search-Space Decomposition-Based SAT Solvers + und Clause Simplifications in Search-Space Decomposition-Based SAT Solvers +
