Clause Simplifications in Search-Space Decomposition-Based SAT Solvers

Tobias PhilippTobias Philipp

Tobias Philipp
Clause Simplifications in Search-Space Decomposition-Based SAT Solvers
In Ulle Endriss, João Leite, eds., 7th European Starting AI Researcher Symposium (STAIRS), volume 264 of Frontiers in Artificial Intelligence and Applications, 211-219, 2014. IOS Press

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: WissensverarbeitungKnowledge Representation and Reasoning

@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}
}