Reducing Symmetries to Generate Easier SAT Instances

Finding countermodels is an effective way of disproving false conjectures. In first-order predicate logic, model finding is an undecidable problem. But if a finite model exists, it can be found by exhaustive search. The finite model generation problem in the first-order logic can also be translated to the satisfiability problem in the propositional logic. But a direct translation may not be very efficient. This paper discusses how to take the symmetries into account so as to make the resulting problem easier. A static method for adding constraints is presented, which can be thought of as an approximation of the least number heuristic (LNH). Also described is a dynamic method, which asks a model searcher like SEM to generate a set of partial models, and then gives each partial model to a propositional prover. The two methods are analyzed, and compared with each other.     

Confirmation-Guided Discovery of First-Order Rules with Tertius

This paper deals with learning first-order logic rules from data lacking an explicit classification predicate. Consequently, the learned rules are not restricted to predicate definitions as in supervised inductive logic programming. First-order logic offers the ability to deal with structured, multi-relational knowledge. Possible applications include first-order knowledge discovery, induction of integrity constraints in databases, multiple predicate learning, and learning mixed theories of predicate definitions and integrity constraints. One of the contributions of our work is a heuristic measure of confirmation, trading off novelty and satisfaction of the rule. The approach has been implemented in the Tertius system. The system performs an optimal best-first search, finding the k most confirmed hypotheses, and includes a non-redundant refinement operator to avoid duplicates in the search. Tertius can be adapted to many different domains by tuning its parameters, and it can deal either with individual-based representations by upgrading propositional representations to first-order, or with general logical rules. We describe a number of experiments demonstrating the feasibility and flexibility of our approach.     

On the constructive orbit problem

Symmetry reduction techniques aim to combat the state-space explosion problem for model checking by restricting search to representative states from equivalence classes with respect to a group of symmetries. The standard approach to representative computation involves converting a state to its minimal image under a permutation group G, before storing the state. This is known as the constructive orbit problem (COP), and is NP{\mathit{NP}} hard. It may be possible to solve the COP efficiently if G is known to have certain structural properties: in particular if G is isomorphic to a full symmetry group, or G is a disjoint/wreath product of subgroups. We extend existing results on solving the COP efficiently for fully symmetric groups, and investigate the problem of automatically classifying an arbitrary permutation group as a disjoint/wreath product of subgroups. We also present an approximate COP strategy based on local search, and some computational group-theoretic optimisations to improve the basic approach of solving the COP by symmetry group enumeration. Experimental results using the TopSPIN symmetry reduction package, which interfaces with the computational group-theoretic system GAP, illustrate the effectiveness of our techniques.     

Excluding Symmetries in Constraint-Based Search

We introduce a new method, called symmetry excluding search (SES), for excluding symmetries in constraint based search. To our knowledge, it is the first declarative method that can be applied to arbitrary symmetries. The SES-method is based on the notion of symmetric constraints, which are used in our modification of a general constraint based search algorithm. The method does not influence the search strategy. Furthermore, it can be used with either the full set of symmetries, or a subset of all symmetries.We proof correctness, completeness and symmetry exclusion properties of our method. Then, we show how to apply the SES-method in the special case of geometric symmetries (rotations and reflections) and permutation symmetries. Furthermore, we give results from practical applications.     

Optimal search-relocation trade-off in Markovian-target searching

In this study, a standard moving-target search model was extended with a multiple-search-speed option, whereby a trade-off is enabled between the increased detection chances owing to the searcher's better location and the increased uncertainty of the target's location resulting from the diminished search performance incurred in the relocation. This enhances the detection probability of the output search path and, thereby, the model's practicality. However, the scalability of the solution method is essential to its implementation, as the basic model is already NP-hard. We developed an efficient heuristic by combining the idea of approximate nondetection probability minimization and a hybridized shortest-path heuristic that exploits the fast-mixing property of the Markov chain. According to the results of an intensive experiment, the heuristic achieves a near-optimal trade-off within a very reasonable computation time.     

Dynamic structural symmetry breaking for constraint satisfaction problems

In recent years, symmetry breaking for constraint satisfaction problems (CSPs) has attracted considerable attention. Various general schemes have been proposed to eliminate symmetries. In general, these schemes may take exponential space or time to eliminate all the symmetries. We identify several classes of CSPs that encompass many practical problems and for which symmetry breaking for various forms of value or variable interchangeability is tractable using dedicated search procedures. We also show the limits of efficient symmetry breaking for such dominance-detection schemes by proving intractability results for some classes of CSPs.     

Parallel Logic Programming for Problem Solving

We present a new model for parallel evaluation of logic programs. This model can exploit the main sources of parallelism that the language of logic expresses: Independent AND parallelism and OR parallelism, together with a secondary source emerging as a consequence of the Independent AND Parallelism: the producer/consumer parallelism. The efficiency is derived from the use of ordered structures for managing the information generated throughout the search process. The model is suitable for evaluating programs with a high degree of non-determinism because it never generates two processes for solving the same subgoal and hence it can exploit the same real parallelism generating a lower number of processes than other models. As an application example, we consider the Job Shop Scheduling problem. We report experimental results showing that logic programs can be designed that exhibit parallelism, and that the use of heuristic information translates into speedup in obtaining answers.     

Detection of rotational and involutional symmetries and congruity of polyhedra

We propose a simple and efficient general algorithm for determining both rotational and involutional symmetries of polyhedra. It requiresO(m ²) time and usesO(m) space, wherem is the number of edges of the polyhedron. As this is the lower bound of the symmetry detection problem for the considered output form, our algorithm is optimal. We show that a slight modification of our symmetry detection algorithm can be used to solve the related conguity problem of polyhedra.     

Symmetry Breaking Constraints for Value Symmetries in Constraint Satisfaction

Constraint satisfaction problems (CSPs) sometimes contain both variable symmetries and value symmetries, causing adverse effects on CSP solvers based on tree search. As a remedy, symmetry breaking constraints are commonly used. While variable symmetry breaking constraints can be expressed easily and propagated efficiently using lexicographic ordering, value symmetry breaking constraints are often difficult to formulate. In this paper, we propose two methods of using symmetry breaking constraints to tackle value symmetries. First, we show theoretically when value symmetries in one CSP correspond to variable symmetries in another CSP of the same problem. We also show when variable symmetry breaking constraints in the two CSPs, combined using channeling constraints, are consistent. Such results allow us to tackle value symmetries efficiently using additional CSP variables and channeling constraints. Second, we introduce value precedence, a notion which can be used to break a common class of value symmetries, namely symmetries of indistinguishable values. While value precedence can be expressed using inefficient if-then constraints in existing CSP solvers, we propose efficient propagation algorithms for implementing global value precedence constraints. We also characterize several theoretical properties of the value precedence constraints. Extensive experiments are conducted to verify the feasibility and efficiency of the two proposals.     

Duality in permutation state spaces and the dual search algorithm

Geometrical symmetries are commonly exploited to improve the efficiency of search algorithms. A new type of symmetry in permutation state spaces, duality, is introduced. Each state has a dual state. Both states share important attributes such as their distance to the goal. Given a state S, it is shown that an admissible heuristic of the dual state of S is an admissible heuristic for S. This provides opportunities for additional heuristic evaluations. An exact definition of the class of problems where duality exists is provided. A new search algorithm, dual search, is presented which switches between the original state and the dual state when it seems likely that the switch will improve the chance of reaching the goal faster. The decision of when to switch is very important and several policies for doing this are investigated. Experimental results show significant improvements for a number of applications, for using the dual state's heuristic evaluation and/or dual search.     

Skeleton-based intrinsic symmetry detection on point clouds

We present a skeleton-based algorithm for intrinsic symmetry detection on imperfect 3D point cloud data. The data imperfections such as noise and incompleteness make it difficult to reliably compute geodesic distances, which play essential roles in existing intrinsic symmetry detection algorithms. In this paper, we leverage recent advances in curve skeleton extraction from point clouds for symmetry detection. Our method exploits the properties of curve skeletons, such as homotopy to the input shape, approximate isometry-invariance, and skeleton-to-surface mapping, for the detection task. Starting from a curve skeleton extracted from an input point cloud, we first compute symmetry electors, each of which is composed of a set of skeleton node pairs pruned with a cascade of symmetry filters. The electors are used to vote for symmetric node pairs indicating the symmetry map on the skeleton. A symmetry correspondence matrix (SCM) is constructed for the input point cloud through transferring the symmetry map from skeleton to point cloud. The final symmetry regions on the point cloud are detected via spectral analysis over the SCM. Experiments on raw point clouds, captured by a 3D scanner or the Microsoft Kinect, demonstrate the robustness of our algorithm. We also apply our method to repair incomplete scans based on the detected intrinsic symmetries.     

T-Resolution: Refinements and Model Elimination

T-resolution is a binary rule, proposed by Policriti and Schwartz in 1995 for theorem proving in first-order theories (T-theorem proving) that can be seen – at least at the ground level – as a variant of Stickel's theory resolution. In this paper we consider refinements of this rule as well as the model elimination variant of it. After a general discussion concerning our viewpoint on theorem proving in first-order theories and a brief comparison with theory resolution, the power and generality of T-resolution are emphasized by introducing suitable linear and ordered refinements, uniformly and in strict analogy with the standard resolution approach. Then a model elimination variant of T-resolution is introduced and proved to be sound and complete; some experimental results are also reported. In the last part of the paper we present two applications of T-resolution: to constraint logic programming and to modal logic.     

Static and dynamic structural symmetry breaking

We reconsider the idea of structural symmetry breaking for constraint satisfaction problems (CSPs). We show that the dynamic dominance checks used in symmetry breaking by dominance-detection search for CSPs with piecewise variable and value symmetries have a static counterpart: there exists a set of constraints that can be posted at the root node and that breaks all the compositions of these (unconditional) symmetries. The amount of these symmetry-breaking constraints is linear in the size of the problem, and yet they are able to remove a super-exponential number of symmetries on both values and variables. Moreover, we compare the search trees under static and dynamic structural symmetry breaking when using fixed variable and value orderings. These results are then generalised to wreath-symmetric CSPs with both variable and value symmetries. We show that there also exists a polynomial-time dominance-detection algorithm for this class of CSPs, as well as a linear-sized set of constraints that breaks these symmetries statically.     

Guarded Fragments with Constants

We prove ExpTime-membership of the satisfiability problem for loosely ∀-guarded first-order formulas with a bounded number of variables and an unbounded number of constants. Guarded fragments with constants are interesting by themselves and because of their connection to hybrid logic.     

Global Intrinsic Symmetries of Shapes

Although considerable attention in recent years has been given to the problem of symmetry detection in general shapes, few methods have been developed that aim to detect and quantify the intrinsic symmetry of a shape rather than its extrinsic, or pose‐dependent symmetry. In this paper, we present a novel approach for efficiently computing symmetries of a shape which are invariant up to isometry preserving transformations. We show that the intrinsic symmetries of a shape are transformed into the Euclidean symmetries in the signature space defined by the eigenfunctions of the Laplace‐Beltrami operator. Based on this observation, we devise an algorithm which detects and computes the isometric mappings from the shape onto itself. We show that our approach is both computationally efficient and robust with respect to small non‐isometric deformations, even if they include topological changes.     

Supporting tensor symmetries in EinSum

Exploiting symmetries are important in numerical mathematics, both with respect to efficient memory usage and with respect to symmetry exploiting algorithms. In this paper, the symmetries of tensors are in focus. A convenient notation for describing coordinate-free tensor symmetries is established, based on sets of permutations. Completely symmetric and antisymmetric tensors are included as special cases. The extensions to multidimensional arrays with other kinds of symmetries or invariant features are also treated.The symmetry information is used to represent tensors with symmetries more economically with respect to memory. In addition, three algorithms that exploit symmetries are presented. First, a Frobenius norm computation is derived. Second, a projection to an index space with general symmetries is shown, and proven to be optimal in the Frobenius norm. Third, a symmetry utilizing formula for a dual mapping between completely antisymmetric index spaces is shown.The implementation of symmetry support in EinSum is discussed. EinSum is a C++ package primarily intended for tensor algebra, capable of supporting the Einstein summation convention. Details on the symmetry part of the implementation are explained. Code for the implementation of the Frobenius norm, the general projection, and the dual mapping is shown, illustrating how symmetry aware software may decrease both the memory usage and the number of arithmetic operations.     

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

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

Satisfying due-dates in the presence of sequence dependent family setups with a special comedown structure

This paper addresses a static, n-job, single-machine scheduling problem with sequence dependent family setups. The setup matrix follows a special structure where a constant setup is required only if a job from a smaller indexed family is an immediate successor of one from a larger indexed family. The objective is to minimize the maximum lateness (L_max). A two-step neighborhood search procedure and an implicit enumeration scheme are proposed. Both procedures exploit the problem structure. The enumeration scheme produces optimum solutions to small and medium sized problems in reasonable computational times, yet it fails to perform efficiently in larger instances. Computational results show that the heuristic procedure is highly effective, and is efficient even for extremely large problems.     

Function symmetries and decoded-PLA realization

Decoded PLA (programmable logic array) has a distinct advantage over ordinary PLA, in that it can realize complex functions with smaller chip area. This paper shows that decoded PLA is particularly suitable if the function to be realized has some form of symmetry. The paper describes a new approach for d-PLA realizations using symmetries. It also describes the computer simulation which helps in the detection and use of such symmetries. Two such realizations are also described.