Sciweavers

SAT
2007
Springer
76views Hardware» more  SAT 2007»
14 years 4 months ago
Satisfiability with Exponential Families
Dominik Scheder, Philipp Zumstein
SAT
2007
Springer
110views Hardware» more  SAT 2007»
14 years 4 months ago
Dynamically Partitioning for Solving QBF
Horst Samulowitz, Fahiem Bacchus
SAT
2007
Springer
146views Hardware» more  SAT 2007»
14 years 4 months ago
Algorithms for Variable-Weighted 2-SAT and Dual Problems
Abstract. In this paper we study NP-hard weighted satisfiability optimization problems for the class 2-CNF providing worst-case upper time bounds. Moreover we consider the monoton...
Stefan Porschen, Ewald Speckenmeyer
SAT
2007
Springer
81views Hardware» more  SAT 2007»
14 years 4 months ago
On the Boolean Connectivity Problem for Horn Relations
Kazuhisa Makino, Suguru Tamaki, Masaki Yamamoto
SAT
2007
Springer
95views Hardware» more  SAT 2007»
14 years 4 months ago
Solving Multi-objective Pseudo-Boolean Problems
Integer Linear Programs are widely used in areas such as routing problems, scheduling analysis and optimization, logic synthesis, and partitioning problems. As many of these proble...
Martin Lukasiewycz, Michael Glaß, Christian ...
SAT
2007
Springer
107views Hardware» more  SAT 2007»
14 years 4 months ago
Combining Adaptive Noise and Look-Ahead in Local Search for SAT
Abstract. The adaptive noise mechanism was introduced in Novelty+ to automatically adapt noise settings during the search [4]. The local search algorithm G2 WSAT deterministically ...
Chu Min Li, Wanxia Wei, Harry Zhang
SAT
2007
Springer
99views Hardware» more  SAT 2007»
14 years 4 months ago
Horn Upper Bounds and Renaming
Abstract. We consider the problem of computing tractable approximations to CNF formulas, extending the approach of Selman and Kautz to compute the Horn-LUB to involve renaming of v...
Marina Langlois, Robert H. Sloan, György Tur&...
SAT
2007
Springer
118views Hardware» more  SAT 2007»
14 years 4 months ago
Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities
Abstract. We continue a study initiated by Kraj´ıˇcek of a Resolutionlike proof system working with clauses of linear inequalities, R(CP). For all proof systems of this kind Kra...
Arist Kojevnikov
SAT
2007
Springer
85views Hardware» more  SAT 2007»
14 years 4 months ago
Effective Incorporation of Double Look-Ahead Procedures
Marijn Heule, Hans van Maaren