Catálogo de publicaciones - libros

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 variables. Negative results are given for the quality of approximation in this extended version. On the other hand, experiments for random 3-CNF show that the new algorithms improve both running time and approximation quality. The output sizes and approximation errors exhibit a ‘Horn bump’ phenomenon: unimodal patterns are observed with maxima in some intermediate range of densities. We also present the results of experiments generating pseudo-random satisfying assignments for Horn formulas.

We study parameterizations of the satisfiability problem for propositional formulas in conjunctive normal form. In particular, we consider two parameters that generalize the notion of matched formulas: (i) the well studied parameter maximum deficiency, and (ii) the size of smallest backdoor sets with respect to certain base classes of bounded maximum deficiency. The simplest base class considered is the class of matched formulas. Our main technical contribution is a hardness result for the detection of weak, strong, and deletion backdoor sets. This result implies, subject to a complexity theoretic assumption, that small backdoor sets with respect to the base classes under consideration cannot be found significantly faster than by exhaustive search.

A promising approach for model counting was recently introduced, which in theory requires the use of large random or parity constraints to obtain near-exact counts of solutions to Boolean formulas. In practice, however, short constraints are preferred as they allow better constraint propagation in SAT solvers. We narrow this gap between theory and practice by presenting experimental evidence that for structured problem domains, very short constraints can lead to probabilistic variance as low as large constraints, and thus provide the same correctness guarantees. We initiate an understanding of this phenomenon by relating it to structural properties of synthetic instances.

Local search achieves good results on a variety of SAT problems and often scales up better than backtrack search. But despite recent advances in local search heuristics it has failed to solve some structured problems, while backtrack search has advanced greatly on such problems. We conjecture that current modelling practices are unintentionally biased in favour of solution by backtrack search. To test this conjecture we remodel two problems whose large instances have long resisted solution by local search: parity learning and Towers of Hanoi as STRIPS planning. By reducing variable dependencies and using other techniques we boost local search performance by several orders of magnitude in both cases, and we can now solve 32-bit and 6-disk instances for the first time using a standard SAT local search algorithm.

The adaptive noise mechanism was introduced in + to automatically adapt noise settings during the search [4]. The local search algorithm deterministically exploits promising decreasing variables to reduce randomness and consequently the dependence on noise parameters. In this paper, we first integrate the adaptive noise mechanism in to obtain an algorithm , whose performance suggests that the deterministic exploitation of promising decreasing variables cooperates well with this mechanism. Then, we propose an approach that uses look-ahead for promising decreasing variables to further reinforce this cooperation. We implement this approach in , resulting in a new local search algorithm called . Without any manual noise or other parameter tuning, shows generally good performance, compared with with approximately optimal static noise settings, or is sometimes even better than . In addition, is favorably compared with state-of-the-art local search algorithms such as ++ and .

This paper shows that idempotents in finite rings of integers can act as Generalized Boolean Assignments (GBA’s) by providing a completeness theorem. We introduce the notion of a generic Generalized Boolean Assignment. The mere propagation of such an assignment reveals feasibility (existence of a solution) of a formula in propositional logic. Then, we demystify this general concept by formulating the process on the bit-level: It turns out that propagation of a GBA only simulates bitwise (non-communicating) parallel computing. We capitalize on this by modifying the state-of-the-art local search solver UnitWalk accordingly. This modification involves a more complicated parallelism.

Fix a set of exponential size, e.g. . The - problem asks whether a propositional formula over variables , ..., has a satisfying assignment . Our interest is in determining the complexity of -. We prove that - is NP-complete for all context-free sets . Furthermore, we show that if - is in P for some exponential , then and all problems in NP have polynomial circuits. This strongly indicates that satisfiability with exponential families is a hard problem. However, we also give an example of an exponential set for which the - problem is not NP-hard, provided .

In this paper we prove an exponential separation between two very similar and natural SAT encodings for the same problem, thereby showing that researchers must be careful when designing encodings, lest they accidentally introduce complexity into the problem being studied. This result provides a formal explanation for empirical results showing that the encoding of a problem can dramatically affect its practical solvability.

We also introduce a domain-independent framework for reasoning about the complexity added to SAT instances by their encodings. This includes the observation that while some encodings may add complexity, other encodings can actually make problems easier to solve by adding clauses which would otherwise be difficult to derive within a Resolution-based SAT-solver. Such encodings can be used as polytime preprocessing to speed up SAT algorithms.

In this paper we study NP-hard variable-weighted satisfiability optimization problems for the class 2-CNF providing worst-case upper time bounds holding for arbitrary real-valued weights. Moreover, we consider the monotone dual class consisting of clause sets where all variables occur at most twice. We show that weighted SAT, XSAT and NAESAT optimization problems for this class are polynomial time solvable using appropriate reductions to specific polynomial time solvable graph problems.

Gopalan et al. studied in ICALP06 [17] connectivity properties of the solution-space of Boolean formulas, and investigated complexity issues on the connectivity problems in Schaefer’s framework. A set of logical relations is if all relations in are either bijunctive, Horn, dual Horn, or affine. They conjectured that the connectivity problem for is in . We disprove their conjecture by showing that there exists a set of Horn relations such that the connectivity problem for is co-complete. We also show that the connectivity problem for bijunctive relations can be solved in ( min {||, ()}) time, where denotes the number of variables, denotes the corresponding 2-CNF formula, and () denotes the time needed to compute the transitive closure of a directed graph of vertices. Furthermore, we investigate a tractable aspect of Horn and dual Horn relations with respect to characteristic sets.