The Implicit Hitting Set (HS) approach has shown very effective for MaxSAT solving. However, only preliminary promising results have been obtained for the very similar Weighted CSP framework. In this paper we contribute towards both a better theoretical understanding of the HS approach and a more effective HS-based solvers for WCSP. First, we bound the minimum number of iterations of HS thanks to what we call distinguished cores. Then, we show a source of inefficiency by introducing two simple problems where HS is unfeasible. Next, we propose two reformulation methods that merge cost-functions to overcome the problem. We provide a theoretical analysis that quantifies the magnitude of the improvement of each method with respect to the number of iterations of the algorithm. In particular, we show that the reformulations can bring an exponential number of iterations down to a constant number in our working examples. Finally, we complement our theoretical analysis with two sets of experiments. First, we show that our results are aligned with real executions. Second, and most importantly, we conduct experiments on typical benchmark problems and show that cost-function merging may be heuristically applied and it may accelerate HS algorithms by several orders of magnitude. In some cases, it even outperforms state-of-the-art solvers.

Abstract MaxSAT, the optimization version of the well-known SAT problem, has attracted a lot of research interest in the past decade. Motivated by the many important applications and inspired by the success of modern SAT solvers, researchers have developed many MaxSAT solvers. Since most research is algorithmic, its significance is mostly evaluated empirically. In this paper, we want to address MaxSAT from the more formal point of view of proof complexity. With that aim, we start providing basic definitions and proving some basic results. Then we analyse the effect of adding split and virtual, two original inference rules, to MaxSAT resolution. We show that each addition makes the resulting proof system stronger, even when virtual is restricted to empty clauses ($0$-virtual). We also analyse the power of our proof systems in the particular case of SAT refutations. We show that our strongest system, ResSV, is equivalent to circular and dual rail with split. We also analyse empirically some known gadget-based reformulations. Our results seem to indicate that the advantage of these three seemingly different systems over general resolution comes mainly from their ability of augmenting the original formula with hypothetical inconsistencies, as captured in a very simple way by the virtual rule.

The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof system with an extension rule. The new proof system MaxResE is sound and complete, and more powerful than plain MaxSAT resolution, since it can refute the soft and hard PHP in polynomial time. We show that MaxResE refutations actually subtract lower bounds from the objective function encoded by the formulas. The resulting formula is the residual after the lower bound extraction. We experimentally show that the residual of the soft PHP (once its necessary cost of 1 has been efficiently subtracted with MaxResE) is a concise, easy to solve, satisfiable problem.

We introduce the concept of local bucket error for the mini-bucket heuristics and show how it can be used to improve the power of AND/OR search for combinatorial optimization tasks in graphical models (e.g. MAP/MPE or weighted CSPs). The local bucket error illuminates how the heuristic errors are distributed in the search space, guided by the mini-bucket heuristic. We present and analyze methods for compiling the local bucket-errors (exactly and approximately) and show that they can be used to yield an effective tool for balancing look-ahead overhead during search. This can be especially instrumental when memory is restricted, accommodating the generation of only weak compiled heuristics. We illustrate the impact of the proposed schemes in an extensive empirical evaluation for both finding exact solutions and anytime suboptimal solutions.

Best-first search can be regarded as anytime scheme for producing lower bounds on the optimal solution, a characteristic that is mostly overlooked. We explore this topic in the context of AND/OR best-first search, guided by the MBE heuristic, when solving graphical models. In that context, the impact of the secondary heuristic for subproblem ordering may be significant, especially in the anytime context. Indeed, our paper illustrates this, showing that the new concept of bucket errors can advise in providing effective subproblem orderings in AND/OR search.

In this paper we introduce MiniMaxSat, a new Max-SAT solver that is built on top of MiniSat+. It incorporates the best current SAT and Max-SAT techniques. It can handle hard clauses(clauses of mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost as in Max-SAT) as well as pseudo-boolean objective functions and constraints. Its main features are: learning and backjumping on hard clauses; resolution-based and substraction-based lower bounding; and lazy propagation with the two-watched literal scheme. Our empirical evaluation comparing a wide set of solving alternatives on a broad set of optimization benchmarks indicates that the performance of MiniMaxSat is usually close to the best specialized alternative and, in some cases, even better.

Variable elimination is a general technique for constraint processing. It is often discarded because of its high space complexity. However, it can be extremely useful when combined with other techniques. In this paper we study the applicability of variable elimination to the challenging problem of finding still-lifes. We illustrate several alternatives: variable elimination as a stand-alone algorithm, interleaved with search, and as a source of good quality lower bounds. We show that these techniques are the best known option both theoretically and empirically. In our experiments we have been able to solve the n=20 instance, which is far beyond reach with alternative approaches.

Graph pattern matching is a central problem in many application fields. Since it is NP-complete, we cannot expect to find algorithms with a good worst-case performance. However, there is still room for general procedures with a good average performance. In this paper we explore four different solving approaches within the constraint satisfaction framework, and introduce a new algorithm, which we call nRF+. The algorithm is a refinement of really full look ahead that takes advantage of the problem structure in order to enhance the look ahead procedure. We give a formal proof that nRF+ is superior to the other approaches in terms of number of visited nodes. An additional contribution of this paper is the introduction of a new benchmark for testing algorithms in this domain. It is formed by a large set of well-defined graphs of very diverse nature. In this benchmark, we show that nRF+ can efficiently solve a broad range of problems, while still leaving many problem instances unsolved. The use of this challenging benchmark is encouraged for future algorithms evaluation.

In this article a new approach to the formalization of inductive inference in terms of non-monotonic inference is proposed. Induction is characterized as closed-world reasoning from the available data, followed by an inductive jump, which consists in assuming that valid conclusions in the database (assuming closed-world) hold also in the rest of the world. This conception of induction results is adequate to characterize those inference processes that could be formalized, that is, those based in analytical procedures of pattern-matching or regularity detection in the available data. the proposed characterization formally describes the implicit deductive processes of induction and its non-monotonic nature, and could be used as an abstract model of the mental process that leads to obtaining inductive hypotheses. This proposal reduces the problem of induction automatization to that of deduction automatization. Also, it constitutes a formal framework that covers several inductive inference methods used in machine learning. Besides it formalizes inductive definitions, which are very common in science and computer science. © 1995 John Wiley & Sons, Inc.