Sciweavers

JSAT
2010
130views more  JSAT 2010»
12 years 10 months ago
DepQBF: A Dependency-Aware QBF Solver
We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quan...
Florian Lonsing, Armin Biere
JSAT
2010
121views more  JSAT 2010»
12 years 10 months ago
Resolution on Quantified Generalized Clause-sets.
This paper is devoted to investigate resolution for quantified generalized clause-sets (QCLS). The soundness and refutation completeness are proved. Then quantified generalized Ho...
Jiwei Jin, Xishun Zhao
JSAT
2010
83views more  JSAT 2010»
12 years 10 months ago
QuBE7.0
In this paper we outline QuBE7's main features, describing first the options of the preprocessors, and then giving some details about how the core search-based solver (i) per...
Enrico Giunchiglia, Paolo Marin, Massimo Narizzano
JSAT
2010
158views more  JSAT 2010»
12 years 10 months ago
Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond
Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has exponential size, and that limited OBDD derivations cannot simulate resolution polynomia...
Olga Tveretina, Carsten Sinz, Hans Zantema
JSAT
2010
87views more  JSAT 2010»
12 years 10 months ago
The Sat4j library, release 2.2
Sat4j is a mature, open source library of SAT-based solvers in Java. It provides a modular SAT solver architecture designed to work with generic constraints. Such architecture is ...
Daniel Le Berre, Anne Parrain
JSAT
2010
119views more  JSAT 2010»
12 years 10 months ago
AQME'10
In this paper we describe aqme'10, the version of the Adaptive QBF Multi-Engine submitted to QBFEVAL'10.
Luca Pulina, Armando Tacchella
JSAT
2010
108views more  JSAT 2010»
12 years 10 months ago
Experiment design and administration for computer clusters for SAT-solvers (EDACC)
The design of a SAT-solver or the modification of an existing one is always followed by a phase of intensive testing of the solver on a benchmark of instances. This task can be ve...
Adrian Balint, Daniel Gall, Gregor Kapler, Robert ...
JSAT
2010
132views more  JSAT 2010»
12 years 10 months ago
The Impact of Max-SAT Resolution-Based Preprocessors on Local Search Solvers
In this paper we analyze three well-known preprocessors for Max-SAT. The first preprocessor is based on the so-called variable saturation. The second preprocessor is based on the ...
Federico Heras, David Bañeres