Iterative and core-guided MaxSAT solving: A survey and assessment

Maximum Satisfiability (MaxSAT) is an optimization version of SAT, and many real world applications can be naturally encoded as such. Solving MaxSAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in developing efficient algorithms and several families of algorithms have been proposed. This paper overviews recent approaches to handle MaxSAT and presents a survey of MaxSAT algorithms based on iteratively calling a SAT solver which are particularly effective to solve problems arising in industrial settings. First, classic algorithms based on iteratively calling a SAT solver and updating a bound are overviewed. Such algorithms are referred to as iterative MaxSAT algorithms. Then, more sophisticated algorithms that additionally take advantage of unsatisfiable cores are described, which are referred to as core-guided MaxSAT algorithms. Core-guided MaxSAT algorithms use the information provided by unsatisfiable cores to relax clauses on demand and to create simpler constraints. Finally, a comprehensive empirical study on non-random benchmarks is conducted, including not only the surveyed algorithms, but also other state-of-the-art MaxSAT solvers. The results indicate that (i) core-guided MaxSAT algorithms in general abort in less instances than classic solvers based on iteratively calling a SAT solver and that (ii) core-guided MaxSAT algorithms are fairly competitive compared to other approaches.     

On the performance of MaxSAT and MinSAT solvers on 2SAT-MaxOnes

We analyze and compare two solvers for Boolean optimization problems: WMaxSatz, a solver for Partial MaxSAT, and MinSatz, a solver for Partial MinSAT. Both MaxSAT and MinSAT are similar, but previous results indicate that when solving optimization problems using both solvers, the performance is quite different on some cases. For getting insights about the differences in the performance of the two solvers, we analyze their behaviour when solving 2SAT-MaxOnes problem instances, given that 2SAT-MaxOnes is probably the most simple, but NP-hard, optimization problem we can solve with them. The analysis is based first on the study of the bounds computed by both algorithms on some particular 2SAT-MaxOnes instances, characterized by the presence of certain particular structures. We find that the fraction of positive literals in the clauses is an important factor regarding the quality of the bounds computed by the algorithms. Then, we also study the importance of this factor on the typical case complexity of Random-p 2SAT-MaxOnes, a variant of the problem where instances are randomly generated with a probability p of having positive literals in the clauses. For the case p=0, the performance results indicate a clear advantage of MinSatz with respect to WMaxSatz, but as we consider positive values of p WMaxSatz starts to show a better performance, although at the same time the typical complexity of Random-p 2SAT-MaxOnes decreases as p increases. We also study the typical value of the bound computed by the two algorithms on these sets of instances, showing that the behaviour is consistent with our analysis of the bounds computed on the particular instances we studied first.     

Quantified maximum satisfiability

In recent years, there have been significant improvements in algorithms both for Quantified Boolean Formulas (QBF) and for Maximum Satisfiability (MaxSAT). This paper studies an optimization extension of QBF and considers the problem in a quantified MaxSAT setting. More precisely, the general QMaxSAT problem is defined for QBFs with a set of soft clausal constraints and consists in finding the largest subset of the soft constraints such that the remaining QBF is true. Two approaches are investigated. One is based on relaxing the soft clauses and performing an iterative search on the cost function. The other approach, which is the main contribution of the paper, is inspired by recent work on MaxSAT, and exploits the iterative identification of unsatisfiable cores. The paper investigates the application of these approaches to the two concrete problems of computing smallest minimal unsatisfiable subformulas (SMUS) and smallest minimal equivalent subformulas (SMES), decision versions of which are well-known problems in the second level of the polynomial hierarchy. Experimental results, obtained on representative problem instances, indicate that the core-guided approach for the SMUS and SMES problems outperforms the use of iterative search over the values of the cost function. More significantly, the core-guided approach to SMUS also outperforms the state-of-the-art SMUS extractor Digger.     

Local-search Extraction of MUSes

SAT is probably one of the most-studied constraint satisfaction problems. In this paper, a new hybrid technique based on local search is introduced in order to approximate and extract minimally unsatisfiable subformulas (in short, MUSes) of unsatisfiable SAT instances. It is based on an original counting heuristic grafted to a local search algorithm, which explores the neighborhood of the current interpretation in an original manner, making use of a critical clause concept. Intuitively, a critical clause is a falsified clause that becomes true thanks to a local search flip only when some other clauses become false at the same time. In the paper, the critical clause concept is investigated. It is shown to be the cornerstone of the efficiency of our approach, which outperforms competing ones to compute MUSes, inconsistent covers and sets of MUSes, most of the time.     

Representations of the language recognition problem for a theorem prover

Two representations of the language recognition problem for a theorem prover in first-order logic are presented and contrasted. One of the representations is based on the familiar method of generating sentential forms of the language, and the other is based on the Cocke parsing algorithm. An augmented theorem prover is described which permits recognition of recursive languages. The state-transformation method developed by Cordell Green to construct problem solutions in resolution-based systems can be used to obtain the parse tree. In particular, the end-order traversal of the parse tree is derived in one of the representations. The paper defines an inference system, termed the cycle inference system, which makes it possible for the theorem prover to model the method on which the representation is based. The general applicability of the cycle inference system to state-space problems is discussed. Given an unsatisfiable setS, where each clause has at most one positive literal, it is shown that there exists an input proof. The clauses for the two representations satisfy these conditions, as do many state-space problems.This work was supported by the National Aeronautics and Space Administration Grant NGR-21-002-270.     

Issues of non-determinism in PROLOG and the Committed Choice Non-Deterministic logic languages

Issues of logic programming have always been bound with those of search. Logic programs are generally thought of as a logical specification of the problem (the declarative reading) in terms of clauses. The inference mechanism of the given logic language provides a means by which the clauses can be used to prove a query to the system (procedural interpretation). The problem of search can be related into forms of non-determinism. That is how to select a possible solution path (clause). It is this criteria that is used to consider the issues of search in PROLOG and the Committed Choice Non-Deterministic execution models.     

Approximate reasoning with credible subsets

The complexity of logical inference in knowledge systems grows with the system size, determined, in particular, by the number of its clauses. This growth is so rapid, that reasoning in sizeable systems becomes intractable.However, given a system S and a query Q, should we be able to detect a subset of S informative enough to provide a correct answer to Q, and small enough to fit into the range of tractable computation,the answer to Q could be produced efficiently. This paper presents a way of implementing this idea.     

How to avoid the derivation of redundant clauses in reasoning systems

This paper addresses two problems concerning the issue of redundant information in resolution based reasoning systems. The first one deals with the question how the derivation of redundant clauses, such as duplicates or instances of already retained clauses, can be substantially reduced. The second one asks for a criterion to decide, which clauses need not be tested for redundancy. We consider a particular kind of redundancy, which we call ancestor subsumption, that is the subsumption of a resolvent by one of its ancestors. It will be shown that the occurrence of cyclic clause sets, which roughly correspond to sets of logical equivalences, accounts for ancestor subsumed resolvents. Moreover, two techniques will be given to cope with the problems caused by such cyclic structures. The first technique, called literal demodulation, uses logical equivalences as rewrite rules, the second one employs a particular kind of theory resolution.     

利用不动点求解子句逻辑推演的Petri网模型

文章研究了子句逻辑推演的Petri网模型表示和不动点求解方法.基于四值逻辑和冲突变迁的概念,可用Horn子句的Petri网模型方法来构造非Horn子句的Petri网模型.逻辑推演的基本方法之一就是寻找逻辑赋值的不动点.该文显示了一种基于Petri网模型的子句逻辑不动点求解算法,比现有算法更为有效.     

基于子句的动态检查强制文字的SAT求解器

检查强制文字是一种重要的预处理方法。结合学习子句,提出一种在求解过程中使用的策略—基于子句的动态检查强制文字(CNL),并且设计了一种易实现低成本的数据结构。分别实现了两个不同版本的求解器:Glucose_PRE和Glucose_CNL,前者在求解初始时将检查强制文字作为预处理,后者实现了基于子句的动态检查强制文字策略。实验测试结果表明,与Glucose_PRE和Glucose3.0求解器相比,求解器Glucose_CNL在求解2015年和2016年SAT竞赛的应用类型的实例时,求解实例个数更多,耗时更少,说明所提策略和所设计的数据结构均可提高求解器的求解性能。     

Benchmark computations based on lattice-Boltzmann,finite element and finite volume methods for laminar flows

The goal of this article is to contribute to the discussion of the efficiency of lattice-Boltzmann (LB) methods as CFD solvers. After a short review of the basic model and extensions, we compare the accuracy and computational efficiency of two research simulation codes based on the LB and the finite-element method (FEM) for two-dimensional incompressible laminar flow problems with complex geometries. We also study the influence of the Mach number on the solution, since LB methods are weakly compressible by nature, by comparing compressible and incompressible results obtained from the LB code and the commercial code CFX. Our results indicate, that for the quantities studied (lift, drag, pressure drop) our LB prototype is competitive for incompressible transient problems, but asymptotically slower for steady-state Stokes flow because the asymptotic algorithmic complexity of the classical LB-method is not optimal compared to the multigrid solvers incorporated in the FEM and CFX code. For the weakly compressible case, the LB approach has a significant wall clock time advantage as compared to CFX. In addition, we demonstrate that the influence of the finite Mach number in LB simulations of incompressible flow is easily underestimated.     

基于不可满足原因的最小纠正集求解

布尔公式的最小纠正集MCS是子句的集合。对于一个不可满足公式,移除MCS后,所得到的新公式可满足。任一MCS中的子句保留在公式中,所得到的新公式不可满足。通过求解MCS 并调整约束集合,能够求解最小不可满足核心、MaxSAT 问题和最大（小）可满足解问题;还能够应用于故障定位、模型检查配置优化等实际问题中。 提出了一种基于不可满足原因的MCS求解算法,实现了相应的CUC工具。通过与目前最好的MCS求解工具LBX进行比较,得到了CUC性能优于LBX的结论。CUC比LBX平均多解出5%（65个）的公式。对于CUC和LBX均可解出的公式,CUC的平均求解时间比LBX快2.5倍。     

使用Petri网T－不变量求解子句的逻辑推论

本文研究了子句逻辑规则的Ｐｅｔｒｉ网模型的表示及使用Ｐｅｔｒｉ网分析方法进行逻辑推论．基于四值逻辑和冲突变迁的概念，表示了非Ｈｏｒｎ子句Ｐｅｔｒｉ网模型的构造，并使用Ｔ－不变量方法解决于句推论问题．另外，本文还显示了向前推论和向后推论在子句Ｐｅｔｒｉ网模型中的应用．     

Solving satisfiability problems with preferences

Propositional satisfiability (SAT) is a success story in Computer Science and Artificial Intelligence: SAT solvers are currently used to solve problems in many different application domains, including planning and formal verification. The main reason for this success is that modern SAT solvers can successfully deal with problems having millions of variables. All these solvers are based on the Davis–Logemann–Loveland procedure (dll). In its original version, dll is a decision procedure, but it can be very easily modified in order to return one or all assignments satisfying the input set of clauses, assuming at least one exists. However, in many cases it is not enough to compute assignments satisfying all the input clauses: Indeed, the returned assignments have also to be “optimal” in some sense, e.g., they have to satisfy as many other constraints—expressed as preferences—as possible. In this paper we start with qualitative preferences on literals, defined as a partially ordered set (poset) of literals. Such a poset induces a poset on total assignments and leads to the definition of optimal model for a formula ψ as a minimal element of the poset on the models of ψ. We show (i) how dll can be extended in order to return one or all optimal models of ψ (once converted in clauses and assuming ψ is satisfiable), and (ii) how the same procedures can be used to compute optimal models wrt a qualitative preference on formulas and/or wrt a quantitative preference on literals or formulas. We implemented our ideas and we tested the resulting system on a variety of very challenging structured benchmarks. The results indicate that our implementation has comparable performances with other state-of-the-art systems, tailored for the specific problems we consider.     

Learning compact Markov logic networks with decision trees

Statistical-relational learning combines logical syntax with probabilistic methods. Markov Logic Networks (MLNs) are a prominent model class that generalizes both first-order logic and undirected graphical models (Markov networks). The qualitative component of an MLN is a set of clauses and the quantitative component is a set of clause weights. Generative MLNs model the joint distribution of relationships and attributes. A state-of-the-art structure learning method is the moralization approach: learn a set of directed Horn clauses, then convert them to conjunctions to obtain MLN clauses. The directed clauses are learned using Bayes net methods. The moralization approach takes advantage of the high-quality inference algorithms for MLNs and their ability to handle cyclic dependencies. A?weakness of moralization is that it leads to an unnecessarily large number of clauses. In this paper we show that using decision trees to represent conditional probabilities in the Bayes net is an effective remedy that leads to much more compact MLN structures. In experiments on benchmark datasets, the decision trees reduce the number of clauses in the moralized MLN by a factor of 5?C25, depending on the dataset. The accuracy of predictions is competitive with the models obtained by standard moralization, and in many cases superior.     

On intractability of the classUP

The classUP [V] is the class of sets accepted by polynomial-time nondeterministic Turing machines which have at most one accepting path for every input. The complexity of this class closely relates to that of computing inverses ofone-way functions, where a one-way function is a one-to-one, length-increasing, and polynomial-time computable function whose inverse cannot be computed within polynomial time. It is known [GS], [K] that there exists a one-way function if and only ifP UP. In this paper the intractability of sets inUP is investigated in terms of polynomial-time reducibility to a sparse set. It is shown thatUP has a set that is _m ^P -reducible to no sparse set ifP UP. We interpret this structural property in the relation with approximation algorithms: it is shown that ifP UP, thenUP has a set with no 1-APT approximation and, furthermore,UP has a set that is not _m ^P -reducible to any set with a 1-APT approximation. The implication of this result in the study of one-way functions is also discussed. In order to prove the main theorem, we introduce a variation of tree-pruning methods.This paper was written while the author visited the Department of Mathematics, University of California, Santa Barbara. This research was supported in part by the National Science Foundation under Grant CCR-8611980.     

Resource-Bounded Paraconsistent Inference

In this paper, a new framework for reasoning from inconsistent propositional belief bases is presented. A family of resource-bounded paraconsistent inference relations is introduced. Such inference relations are based on S-3 entailment, an inference relation logically weaker than the classical one and parametrized by a set S of propositional variables. The computational complexity of our relations is identified, and their logical properties are analyzed. Among the strong features of our framework is the fact that tractability is ensured each time |S| is bounded and a limited amount of knowledge is taken into account within the belief base. Furthermore, binary connectives , behave in a classical manner. Finally, our framework is general enough to encompass several paraconsistent multi-valued logics (including S-3, J ₃ and its restrictions), the standard coherence-based approach to inconsistency handling (based on the selection of consistent subbases) and some signed systems for paraconsistent reasoning as specific cases.     

Reducing signed propositional formulas

 New strategies of reduction for finite-valued propositional logics are introduced in the framework of the TAS¹ methodology developed by the authors [1]. A new data structure, the Δ^-sets, is introduced to store information about the formula being analysed, and its usefulness is shown by developing efficient strategies to decrease the size of signed propositional formulas, viz., new criteria to detect the validity or unsatisfiability of subformulas, and a strong generalisation of the pure literal rule.     

Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures

Recently Lee and Plaisted proposed a theorem-proving method, the hyperlinking proof procedure, to eliminate duplication of instances of clauses during the process of inference. A theorem prover, CLIN, which implements the procedure was also constructed. In this implementation, redundant work on literal unification checking, partial unification checking, and duplicate instance checking is performed repetitively, resulting in a large overhead when many rounds of hyperlinking are needed for an input problem. We propose a technique that maintains information across rounds in shared network structures, so that the redundant work in each hyperlinking round can be avoided. Empirical performance comparison has been done between CLIN and CLIN-net, which is the theorem prover with shared network structures, and some results are shown. Problems related to memory overhead and literal ordering are discussed.Supported by National Science Council under grants NSC 81-0408-E-110-509 and NSC-82-0408-E-110-045. A preliminary version of this paper appeared in Proceedings of International Conference on Computing and Information (Sudbury, Ontario Canada, May 1993).     

A probabilistic interpretation of the medical expert system CADIAG-2

CADIAG-2 is a well-known expert system aimed at providing support for medical diagnose in the field of internal medicine. CADIAG-2 consists of a knowledge base in the form of a set of IF-THEN rules that relate distinct medical entities, in this paper interpreted as conditional probabilistic statements, and an inference engine constructed upon methods of fuzzy set theory. The aim underlying this paper is the understanding of the logical structure of the inference in CADIAG-2. To that purpose, we provide a (probabilistic) logical formalisation of the inference of the system and check its adequacy with probabilistic logic.