Catálogo de publicaciones - libros

Compared to SAT, there is no simple concept of what a solution to a QBF problem is. Furthermore, as the series of QBF evaluations shows, the QBF solvers that are available often disagree. Thus, proof generation for QBF seems to be even more important than for SAT. In this paper we propose a new uniform proof format, which captures refutations and witnesses for a variety of QBF solvers, and is based on a novel extended resolution rule for QBF. Our experiments show the flexibility of this new format. We also identify shortcomings of our format and conjecture that a purely resolution based proof calculus is not powerful enough to trace the most efficient solvers.

In this paper we present a new technique to solve Quantified Boolean Formulas (QBF). Our technique applies the idea of dynamic partitioning to QBF solvers. Dynamic partitioning has previously been utilized in #SAT solvers that count the number of models of a propositional formula. One of the main differences with the #SAT case comes from the solution learning techniques employed in search based QBF solvers. Extending solution learning to a partitioning solver involves some considerable complexities which we show how to resolve. We have implemented our ideas in a new QBF solver, and demonstrate that dynamic partitioning is able to increase the performance of search based solvers, sometimes significantly. Empirically our new solver offers performance that is superior to other search based solvers and in many cases superior to non-search based solvers.

We generalize the notion of backdoor sets from propositional formulas to quantified Boolean formulas in conjunctive normal form (QCNF). We develop parameterized algorithms that admit uniform polynomial time QCNF evaluation parameterized by the size of smallest strong backdoor sets. For our algorithms we develop a theory of variable dependency which is of independent interest. As a result, we obtain hierarchies of classes of tractable QCNF formulas with the classes of quantified Horn and quantified 2CNF formulas, respectively, at their first level, thus gradually generalizing these two prominent tractable classes. In contrast to known tractable classes based on bounded treewidth, the number of quantifier alternations of our classes is unbounded.

We present a new approach for preprocessing Quantified Boolean Formulas () in conjunctive normal form () by expanding a selection of universally quantified variables with bounded expansion costs. We describe a suitable selection strategy which exploits locality of universals and combines cost estimates with goal orientation by taking into account unit literals which might be obtained.

Furthermore, we investigate how Q-resolution can be integrated into this method. In particular, resolution is applied specifically to reduce the amount of copying necessary for universal expansion.

Experimental results demonstrate that our preprocessing can successfully improve the performance of state-of-the-art solvers on well-known problems from the QBFLIB collection.

We introduce an adaptive algorithm to control the use of the double look-ahead procedure. This procedure sometimes enhances the performance of look-ahead based satisfiability solvers. Current use of this procedure is driven by static heuristics. Experiments show that over a wide variety of instances, different parameter settings result in optimal performance. Moreover, a strategy that yields fast performance on one particular class of instances may cause a significant slowdown on other families. Using a single adaptive strategy, we accomplish performances close to the optimal performances reached by the various static settings. On some families, we clearly outperform even the fastest performance based on static heuristics. This paper provides a description of the algorithm and a comparison with the static strategies. This method is incorporated in march_dl, satz, and kcnfs. Also, the dynamic behavior of the algorithm is illustrated by adaptation plots on various benchmarks.

SAT solvers are often challenged with very hard problems that remain unsolved after hours of CPU time. The research community meets the challenge in two ways: (1) by improving the SAT solver technology, for example, perfecting heuristics for variable ordering, and (2) by inventing new ways of constructing simpler SAT problems, either using domain specific information during the translation from the original problem to CNF, or by applying a more universal CNF simplification procedure after the translation. This paper explores preprocessing of circuit-based SAT problems using recent advances in logic synthesis. Two fast logic synthesis techniques are considered: DAG-aware logic minimization and a novel type of structural technology mapping, which reduces the size of the CNF derived from the circuit. These techniques are experimentally compared to CNF-based preprocessing. The conclusion is that the proposed techniques are complementary to CNF-based preprocessing and speedup SAT solving substantially on industrial examples.

We show that modern conflict-driven SAT solvers implicitly build and prune a decision tree whose nodes are associated with flipped variables. Practical usefulness of conflict-driven learning schemes, like 1UIP or UIP, depends on their ability to guide the solver towards refutations associated with compact decision trees. We propose an enhancement of 1UIP that is empirically helpful for real-world industrial benchmarks.

We introduce in this paper a lightweight technique for reducing work repetition caused by non–chronological backtracking commonly practiced by DPLL–based SAT solvers. The presented technique can be viewed as a partial component caching scheme. Empirical evaluation of the technique reveals significant improvements on a broad range of industrial instances.

We present an algorithm for finding a smallest Resolution refutation of any 2CNF in polynomial time.

We study , where for every clause  ∈  we have , i.e., is closed under elementwise complementation of clauses. The of a clause-set is defined as , where () = () − () is the difference of the number of clauses and the number of variables, while the is := max(′) ≥ 0. We show polynomial time SAT decision for complement-invariant clause-sets with , exploiting the (non-trivial) decision algorithm for sign-non-singular (SNS) matrices given by [Robertson, Seymour, Thomas 1999; McCuaig 2004]. As an application, hypergraph 2-colourability decision is considered. Minimally unsatisfiable complement-invariant clause-sets fulfil , and thus we immediately obtain polynomial time decidability of minimally unsatisfiable complement-invariant clause-sets with () = 0, but we also give more direct algorithms and characterisations (especially for sub-classes). The theory of autarkies is the basis for all these considerations.