Catálogo de publicaciones - libros

The (WCSP) framework is a soft constraint framework which can model many real life optimization or over-constrained problems. While there are many local consistency notions available to speed up WCSP solving, in this paper, we investigate how to effectively combine and channel mutually redundant WCSP models to increase constraint propagation. This successful technique for reducing search space in classical constraint satisfaction has been shown non-trivial when adapted for the WCSP framework. We propose a parameterized local consistency LB(,), which can be instantiated with local consistency for single models and applied to a combined model with sub-models, and also provide a simple algorithm to enforce it. We instantiate LB(,) with different state-of-the-art local consistencies AC*, FDAC*, and EDAC*, and demonstrate empirically the efficiency of the algorithm using different benchmark problems.

We present a variant of the Weighted Maximum Satisfiability Problem (Weighted Max-SAT), which is a modeling of the Semiring Constraint Satisfaction framework. We show how to encode a Semiring Constraint Satisfaction Problem (SCSP) into an instance of a propositional Weighted Max-SAT, and call the encoding Weighted Semiring Max-SAT (WS-Max-SAT). The clauses in our encoding are highly structured and we exploit this feature to develop two algorithms for solving WS-Max-SAT: an incomplete algorithm based on the well-known GSAT algorithm for Max-SAT, and a branch-and-bound algorithm which is complete. Our preliminary experiments show that the translation of SCSP into WS-Max-SAT is feasible, and that our branch-and-bound algorithm performs surprisingly well. We aim in future to combine the natural flexible representation of the SCSP framework with the inherent efficiencies of SAT solvers by adjusting existing SAT solvers to solve WS-Max-SAT.

In this paper we describe a stochastic local search (SLS) procedure for finding satisfying models of satisfiable propositional formulae. This new algorithm, gNovelty, draws on the features of two other WalkSAT family algorithms: R+AdaptNovelty and GWSAT, while also successfully employing a dynamic local search (DLS) clause weighting heuristic to further improve performance.

gNovelty was a Gold Medal winner in the random category of the 2007 SAT competition. In this paper we present a detailed description of the algorithm and extend the SAT competition results via an empirical study of the effects of problem structure and parameter tuning on the performance of gNovelty. The study also compares gNovelty with two of the most representative WalkSAT-based solvers: GWSAT, AdaptNovelty, and two of the most representative DLS solvers: RSAPS and PAWS. Our new results augment the SAT competition results and show that gNovelty is also highly competitive in the domain of solving satisfiability problems in comparison with other SLS techniques.

We introduce a new branch-and-bound Max-SAT solver, Clone, which employs a novel approach for computing lower bounds. This approach allows Clone to search in a reduced space. Moreover, Clone is equipped with novel techniques for learning from soft conflicts. Experimental results show that Clone performs competitively with the leading Max-SAT solver in the broadest category of this year’s Max-SAT evaluation and outperforms last year’s leading solvers.

We study the first level of a conjunctive normal form (CNF) formula hierarchy with respect to the propositional satisfiability problem (SAT). This hierarchy is defined over a base formula that we call a . Such a hypercube simply consists of all 2 possible -clauses over a given set of Boolean variables. The first level of the hierarchy are , meaning that arbitrary hypercubes are joined together via taking from each arbitrary many clauses for joining, i.e., set-union, such that each chosen clause occurs in at most one new clause of the 1-hyperjoin. We prove that arbitrary 1-hyperjoins can efficiently be recognized and solved w.r.t. SAT. To that end we introduce a simple closure concept on the set of the propositional variables of a formula.

Planning as satisfiability is a powerful approach to solving domain independent planning problems. In this paper, we consider a relaxed semantics for plans with parallel operator application based on -step semantics. Operators can be applied in parallel if there is at least one ordering in which they can be sequentially executed. Under certain conditions, we allow them to be executed simultaneously in a state even if not all of them are applicable in . In this case, we guarantee that they are enabled by other operators that are applied at the same time point. We formalize the semantics of parallel plans in this setting, and propose an effective translation for STRIPS problems into the propositional logic. We finally show that this relaxed semantics yields an approach to classical planning that is sometimes much more efficient than the existing SAT-based planners.

We present a new forgetting method in logic programs with ordered disjunction (LPODs). To forget a literal means to give it up from the answer sets of the program. There is a known method for doing this in an extended logic program (ELP) by transforming it into another such program whose answer sets have only lost the forgotten literal. However, a naive application of it to an LPOD can produce undesirable results. Our new method avoids these, and ensures that the answer sets of the LPOD, as specified by its so-called split programs, only lose as few literals as are necessary. To achieve this we introduce two new literals and into the syntax of LPODs and extend the definition of an answer set accordingly.

This paper investigates the modality ‘true by default’, associating it with those propositions which hold over a ‘majority’ of possible worlds. A semantic account of ‘majorities’ as the ‘large subsets’ of a set is furnished, and a modal logic of ‘majority default reasoning’ based on this semantics is axiomatised and proved sound and complete.

Anti-unification has often be used as a tool for analogy making. But while first-order anti-unification is too simple for many applications, general higher-order anti-unification is too complex and leads into theoretical difficulties. In this paper we present a restricted framework for higher-order substitutions and show that anti-unification is well-defined in this setting. A complexity measure for generalizations can be introduced in a quite natural way, which allows for selecting preferred generalizations. An algorithm for computing such generalizations is presented and the utility of complexity for anti-unifying sets of terms is discussed by an extended example.

Transposition tables have long been a viable tool in the pruning mechanisms of game-tree search algorithms. In such applications, a transposition table can reduce a game-tree to a game-graph with unique board positions at the nodes. This paper proposes a transposition table extension, called a table, where templates that prove winning positions are used to map features of board positions to board values. This paper demonstrates that a game-tree search for the game of Hex can have a more effective pruning mechanism using a template matching table than it does using a transposition table.