Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings

Much excitement has been generated by the success of stochastic local search procedures at finding solutions to large, very hard satisfiability problems. Many of the problems on which these procedures have been effective are non-Boolean in that they are most naturally formulated in terms of variables with domain sizes greater than two. Approaches to solving non-Boolean satisfiability problems fall into two categories. In the direct approach, the problem is tackled by an algorithm for non-Boolean problems. In the transformation approach, the non-Boolean problem is reformulated as an equivalent Boolean problem and then a Boolean solver is used. This paper compares four methods for solving non-Boolean problems: one direct and three transformational. The comparison first examines the search spaces confronted by the four methods, and then tests their ability to solve random formulas, the round-robin sports scheduling problem, and the quasigroup completion problem. The experiments show that the relative performance of the methods depends on the domain size of the problem and that the direct method scales better as domain size increases. Along the route to performing these comparisons we make three other contributions. First, we generalize Walksat, a highly successful stochastic local search procedure for Boolean satisfiability problems, to work on problems with domains of any finite size. Second, we introduce a new method for transforming non-Boolean problems to Boolean problems and improve on an existing transformation. Third, we identify sufficient conditions for omitting at-least-one and at-most-one clauses from a transformed formula. Fourth, for use in our experiments we propose a model for generating random formulas that vary in domain size but are similar in other respects.     

Improving exact algorithms for MAX-2-SAT

We study three new techniques that will speed up the branch-and-bound algorithm for the MAX-2-SAT problem: The first technique is a group of new lower bound functions for the algorithm and we show that these functions are admissible and consistently better than other known lower bound functions. The other two techniques are based on the strongly connected components of the implication graph of a 2CNF formula: One uses the graph to simplify the formula and the other uses the graph to design a new variable ordering. The experiments show that the simplification can reduce the size of the input substantially no matter what is the clause-to-variable ratio and that the new variable ordering performs much better when the clause-to-variable ratio is less than 2. A direct outcome of this research is a high-performance implementation of an exact algorithm for MAX-2-SAT which outperforms any implementation we know about in the same category. We also show that our implementation is a feasible and effective tool to solve large instances of the Max-Cut problem in graph theory.Preliminary results of this paper appeared in [20,21]. This research was supported in part by NSF under grant CCR-0098093.     

Efficient data structures for backtrack search SAT solvers

The implementation of efficient Propositional Satisfiability (SAT) solvers entails the utilization of highly efficient data structures, as illustrated by most of the recent state-of-the-art SAT solvers. However, it is in general hard to compare existing data structures, since different solvers are often characterized by fairly different algorithmic organizations and techniques, and by different search strategies and heuristics. This paper aims the evaluation of data structures for backtrack search SAT solvers, under a common unbiased SAT framework. In addition, advantages and drawbacks of each existing data structure are identified. Finally, new data structures are proposed, that are competitive with the most efficient data structures currently available, and that may be preferable for the next generation SAT solvers.     

Efficient data structures for backtrack search SAT solvers

The implementation of efficient Propositional Satisfiability (SAT) solvers entails the utilization of highly efficient data structures, as illustrated by most of the recent state-of-the-art SAT solvers. However, it is in general hard to compare existing data structures, since different solvers are often characterized by fairly different algorithmic organizations and techniques, and by different search strategies and heuristics. This paper aims the evaluation of data structures for backtrack search SAT solvers, under a common unbiased SAT framework. In addition, advantages and drawbacks of each existing data structure are identified. Finally, new data structures are proposed, that are competitive with the most efficient data structures currently available, and that may be preferable for the next generation SAT solvers.     

Answer Set Programming Based on Propositional Satisfiability

Answer set programming (ASP) emerged in the late 1990s as a new logic programming paradigm that has been successfully applied in various application domains. Also motivated by the availability of efficient solvers for propositional satisfiability (SAT), various reductions from logic programs to SAT were introduced. All these reductions, however, are limited to a subclass of logic programs or introduce new variables or may produce exponentially bigger propositional formulas. In this paper, we present a SAT-based procedure, called ASPSAT, that (1) deals with any (nondisjunctive) logic program, (2) works on a propositional formula without additional variables (except for those possibly introduced by the clause form transformation), and (3) is guaranteed to work in polynomial space. From a theoretical perspective, we prove soundness and completeness of ASPSAT. From a practical perspective, we have (1) implemented ASPSAT in Cmodels, (2) extended the basic procedures in order to incorporate the most popular SAT reasoning strategies, and (3) conducted an extensive comparative analysis involving other state-of-the-art answer set solvers. The experimental analysis shows that our solver is competitive with the other solvers we considered and that the reasoning strategies that work best on ‘small but hard’ problems are ineffective on ‘big but easy’ problems and vice versa.     

The Propositional Formula Checker HeerHugo

HeerHugo is a propositional formula checker that determines whether a given formula is satisfiable or not. The underlying algorithm is based on a specific breadth-first search procedure, with several enhancements including unit resolution and 2-satisfiability tests. Its main ingredient is the branch/merge rule inspired by an algorithm proposed by Stållmarck, which is protected by a software patent. In this paper, the main elements of the algorithm are discussed, and its remarkable effectiveness is illustrated with some examples and computational results.     

由一阶逻辑公式得到命题逻辑可满足性问题实例

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.     

半扩展规则下分解的定理证明方法

基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.IER(improved extension rule)算法是不完备的算法,在判定子句集子空间不可满足时,并不能判定子句集的满足性,算法还需重新调用ER(extension rule)算法,降低了算法的求解效率.通过对子句集的极大项空间的研究,给出了子句集的极大项空间分解后子空间的求解方法.通过对扩展规则的研究,给出了极大项部分空间可满足性判定方法PSER(partial semi-extension rule).在IER算法判定子空间不可满足时,可以调用PSER算法判定子空间对应的补空间的可满足性,从而得到子句集的可满足性,避免了不能判定极大项子空间可满足性时需重新调用ER算法的缺点,使得IER算法更完备.在此基础上,还提出DPSER(degree partial semi-extension rule)定理证明方法.实验结果表明:所提出的DPSER和IPSER的执行效率较基于归结的有向归结算法DR、IER及NER算法有明显的提高.     

基于自动推理技术的智能规划方法

对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规划方法,并结合国际规划竞赛和相关论文等的实验结论说明上述方法的有效性和可行性.最后,提出目前基于自动推理技术的智能规划方法所面临的挑战、可能的处理方法以及与之相关的研究热点与趋势.     

模态逻辑推理的翻译方法

文中研究了模态逻辑推理的翻译法，即把模态逻辑公式按照一定的规则翻译成经典逻辑公式，再用传统的定理器进行推理，文中指出，该方法在理论上保持了正规命题模态逻辑的可判定性，还给出了一些试验结果，说明该方法实际可行的。     

基于消息传递关系网络的布尔可满足性预测

布尔可满足性求解能够验证的问题规模通常受限, 因此, 如何高精度地预测布尔可满足性问题的可满足性是一个重要研究问题, 也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构, 但是这种表征方法缺少了变量、子句之间的重要关系信息.在我们的方法中, 通过将原始布尔可满足性问题实例表征为多关系异构图的方式来表达变量和句子之间的关系, 并设计使用消息传递关系网络模型来捕获实例的关系信息, 提取了更多的结构特征.结果表明, 该模型在预测精度、泛化能力和资源需求等方面均优于现有模型, 对所选数据集的平均预测精度为81%.该模型在小规模问题(变量数为100)上训练, 在大规模数据集上预测的平均预测精度达到了80.8%.同时, 该模型对随机生成的非均匀随机问题的预测精度达到99%, 这意味着它学习了预测可满足性的重要特征.此外, 模型预测所花费的时间随着问题规模的增大也只是呈线性增长. 总结而言, 本文基于关系消息传递网络提出了一个预测精度更高, 泛化能力更好的布尔可满足性预测方法.     

Algorithms for Testing Satisfiability Formulas

The present paper presents algorithms for testing satisfiabily of clausalformulas in the propositional logic and the firs-order logic. The algorithmbased on the enumeration of solutions for testing the satisfiability ofpropositional formula, has already been given by K. Iwama, O. Dubois. Theoriginality in this paper is to combine this algorithm to other procedures,especially with the pure-literal literal and the one-literal rule, and also theone which consists in changing any formulas in formulas bounded. Thealgorithm based on the enumeration of the solution combined to theseprocedures is more efficient. The algorithm based on the concept ofresolutive derivation from Skolem normal form of formula in first-order logic, has already been given. The idea in present's paper is tocombined to this algorithm to process of elimination of tautological clausesand process of elimination of subsumed clauses.     

可满足问题中的模型计数

模型计数问题是指计算给定问题的解的个数,这是一类比决策更困难的问题,也是人工智能领域研究的一个热点问题.对模型计数问题的研究不仅可以提高算法的求解效率,更能促进对问题困难本质的了解.以可满足问题（命题可满足（SAT）和约束可满足问题（CSP））为例,从精确算法和近似求解两方面综述了模型计数问题的研究现状,重点介绍了相关概念以及各个算法之间的优缺点,并提出了有待解决的开放性问题,对模型计数问题的研究予以了总结和展望.     

基于树宽的警示传播算法收敛性分析

警示传播算法作为一种基本的信息传播算法,其收敛时求解可满足性问题十分有效,但因子图结构较为复杂时,算法往往不收敛导致求解失败。为了对这种现象给予理论解释,同时对警示传播算法收敛性进行有效分析,利用树分解方法构造了命题公式对应因子图的树宽度量模型,计算可满足随机实例的树宽。建立树宽与警示传播算法收敛性之间的关系,给出了基于树宽的警示传播算法收敛性判定条件。通过实验分析,结果表明该方法有效,对于分析其他信息传播算法收敛性分析研究具有十分重要的意义。     

基于结构熵的警示传播算法收敛性分析

收敛性是评价信息传播算法性能的重要指标,信息传播算法求解可满足性问题时,命题公式的结构特征影响算法的收敛性,具有复杂结构的命题公式,信息传播算法不总收敛。为了系统地对此现象给予理论解释,借助于结构熵的方法和技术,提出命题公式的结构熵模型及其度量方法,计算随机可满足性实例的结构熵。警示传播算法(WP)作为信息传播算法的基本模型,分析WP算法的收敛性对于研究其他信息传播算法的收敛性具有重要意义,分析了WP算法收敛性与结构熵之间的关系,给出WP算法收敛的判定条件。通过实验分析,该方法有效可行。     

Implementing the Davis–Putnam Method

The method proposed by Davis, Putnam, Logemann, and Loveland for propositional reasoning, often referred to as the Davis–Putnam method, is one of the major practical methods for the satisfiability (SAT) problem of propositional logic. We show how to implement the Davis–Putnam method efficiently using the trie data structure for propositional clauses. A new technique of indexing only the first and last literals of clauses yields a unit propagation procedure whose complexity is sublinear to the number of occurrences of the variable in the input. We also show that the Davis–Putnam method can work better when unit subsumption is not used. We illustrate the performance of our programs on some quasigroup problems. The efficiency of our programs has enabled us to solve some open quasigroup problems.     

一种新的基于扩展规则的定理证明算法

基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法,首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时问和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.     

命题逻辑的子句集中文字的分类

检测和消除命题逻辑公式中的冗余文字,是人工智能领域广泛研究的基本问题。针对命题逻辑的子句集中子句的划分,结合冗余子句和冗余文字的概念,将命题逻辑的子句集中的文字分为必需文字、有用文字和无用文字3类,并分别给出其定义。讨论3种文字与无冗余等价子集的性质,给出其等价子集的等价描述方法。得到题逻辑的子句集中必需文字、有用文字和无用文字的判定方法,借助子句集的可满足性得到3种文字与子句集的可满足性的等价条件。上述结果对命题逻辑中文字属性的判断提供了多种可选择方法,同时为命题逻辑公式的化简奠定了理论基础。     

Probability logic and optimization SAT: The PSAT and CPA models

Both probabilistic satisfiability (PSAT) and the check of coherence of probability assessment (CPA) can be considered as probabilistic counterparts of the classical propositional satisfiability problem (SAT). Actually, CPA turns out to be a particular case of PSAT; in this paper, we compare the computational complexity of these two problems for some classes of instances. First, we point out the relations between these probabilistic problems and two well known optimization counterparts of SAT, namely Max SAT and Min SAT. We then prove that Max SAT with unrestricted weights is NP-hard for the class of graph formulas, where Min SAT can be solved in polynomial time. In light of the aforementioned relations, we conclude that PSAT is NP-complete for ideal formulas, where CPA can be solved in linear time.