Sciweavers

SAT
2010
Springer
127views Hardware» more  SAT 2010»
13 years 9 months ago
Symmetry and Satisfiability: An Update
Abstract. The past few years have seen significant progress in algorithms and heuristics for both SAT and symmetry detection. Additionally, the thesis that some of SAT's intra...
Hadi Katebi, Karem A. Sakallah, Igor L. Markov
SAT
2010
Springer
165views Hardware» more  SAT 2010»
13 years 9 months ago
An Empirical Study of Optimal Noise and Runtime Distributions in Local Search
This paper presents a detailed empirical study of local search for Boolean satisfiability (SAT), highlighting several interesting properties, some of which were previously unknown...
Lukas Kroc, Ashish Sabharwal, Bart Selman
SAT
2010
Springer
172views Hardware» more  SAT 2010»
13 years 9 months ago
On the Relative Merits of Simple Local Search Methods for the MAX-SAT Problem
Algorithms based on local search are popular for solving many optimization problems including the maximum satisfiability problem (MAXSAT). With regard to MAXSAT, the state of the ...
Denis Pankratov, Allan Borodin
SAT
2010
Springer
152views Hardware» more  SAT 2010»
13 years 9 months ago
Simple but Hard Mixed Horn Formulas
Abstract. We study simple classes of mixed Horn formulas, in which the structure of the Horn part is drastically constrained. We show that the SAT problem for formulas in these cla...
Gayathri Namasivayam, Miroslaw Truszczynski
SAT
2010
Springer
132views Hardware» more  SAT 2010»
13 years 9 months ago
Exploiting Circuit Representations in QBF Solving
Previous work has shown that circuit representations can be exploited in QBF solvers to obtain useful performance improvements. In this paper we examine some additional techniques ...
Alexandra Goultiaeva, Fahiem Bacchus
SAT
2010
Springer
174views Hardware» more  SAT 2010»
13 years 9 months ago
A System for Solving Constraint Satisfaction Problems with SMT
Abstract. SAT Modulo Theories (SMT) consists of deciding the satisfiability of a formula with respect to a decidable background theory, such as linear integer arithmetic, bit-vect...
Miquel Bofill, Josep Suy, Mateu Villaret
SAT
2010
Springer
136views Hardware» more  SAT 2010»
14 years 3 months ago
A Non-prenex, Non-clausal QBF Solver with Game-State Learning
Abstract. We describe a DPLL-based solver for the problem of quantified boolean formulas (QBF) in non-prenex, non-CNF form. We make two contributions. First, we reformulate clause...
William Klieber, Samir Sapra, Sicun Gao, Edmund M....
SAT
2010
Springer
194views Hardware» more  SAT 2010»
14 years 3 months ago
Integrating Dependency Schemes in Search-Based QBF Solvers
Florian Lonsing, Armin Biere
SAT
2010
Springer
160views Hardware» more  SAT 2010»
14 years 3 months ago
Reconstructing Solutions after Blocked Clause Elimination
Abstract. Preprocessing has proven important in enabling efficient Boolean satisfiability (SAT) solving. For many real application scenarios of SAT it is important to be able to ...
Matti Järvisalo, Armin Biere