Search

Gradual patterns extract useful knowledge from numerical databases as attribute co-variations. This article introduces a constraint-based modeling framework for the problem of extracting frequent gradual patterns from numerical data. Our declarative framework provides a principle way to take advantage of recent advancements in satisfiability testing and several features of modern SAT solvers to enumerating gradual patterns from input data. Interestingly, our approach can easily be extended to accommodate additional requirements, including temporal constraints, enabling the extraction of more specific patterns across a wide spectrum of gradual pattern mining applications. An empirical evaluation conducted on two real-world datasets demonstrates the efficacy of the proposed approach.

In this paper, we address the issue of designing from SAT new value ordering heuristics for CSP. We show that using the direct and support SAT encodings of CSP instances, such heuristics can be naturally derived from the well-known two-sided Jeroslow-Wangheuristic. These heuristics exploit the bi-directionality of constraint supports to give a more comprehensive picture in terms of domain reduction when a given value is assigned to (resp. removed from) a given variable. Interestingly, in the context of a backtracking search algorithm that exploits binary branching and the adaptive variable ordering heuristic dom/wdeg, we experimentally observed that the new heuristics yielded the best results on satisfiable and unsatisfiable instances when following the promise and the fail-first policies, respectively.

In this paper, nogood recording is investigated for CSP within the randomization and restart framework. Our goal is to avoid the same situations to occur from one run to the next ones. More precisely, nogoods are recorded when the current cutoff value is reached, i.e. before restarting the search algorithm. Such a set of nogoods is extracted from the last branch of the current search tree and exploited using the structure of watched literals originally proposed for SAT. We prove that the worst-case time complexity of extracting such nogoods at the end of each run is only O(n2d)where nis the number of variables of the constraint network and dthe size of the greatest domain, whereas for any node of the search tree, the worst-case time complexity of exploiting these nogoods to enforce Generalized Arc Consistency (GAC) is O(n|B|)where |B|denotes the number of recorded nogoods. As the number of nogoods recorded before each new run is bounded by the length of the last branch, the total number of recorded nogoods is polynomial in the number of restarts. Interestingly, we show that when the minimization of the nogoods is envisioned with respect to an inference operator ?, it is possible to directly identify some nogoods that cannot be minimized. For ?=AC(i.e. for MAC), the worst-case time complexity of extracting minimal nogoods is slightly increased to O(en2d3)where eis the number of constraints of the network. Experimentation over a wide range of CSP instances using a generic state-of-the-art CSP solver demonstrates the effectiveness of this approach. Recording nogoods (and in particular, minimal nogoods) from restarts significantly improves the robustness of the solver.

In this paper, an efficient heuristic allowing one to localize inconsistent kernels in propositional knowledge‐bases is described. Then, it is shown that local search techniques can boost the performance of logically complete methods for SAT. More precisely, local search techniques can be used to guide the branching strategy of logically complete techniques like Davis and Putnam's one, giving rise to significant performance improvements, in particular when addressing locally inconsistent problems. Moreover, this approach appears very competitive in the context of consistent SAT instances, too.