Narrow Results

Preprocessing techniques play a great role in efficient propositional solving and clause elimination methods are significant parts of them, which speed up SAT solvers’ solving process by deleting redundant clauses in CNF formulas without influencing the satisfiability or unsatisfiability of the original formulas. In this paper, a novel theoretical principle of clause elimination multi-literal implication modulo resolution (MIMR) is put forward. Its soundness proof is also given, to prove any clause satisfying the principle of MIMR is redundant. Besides, effectiveness of MIMR is discussed compared with that of implication modulo resolution (IMR), which is higher than that of IMR.

This paper is about the analysis of sets of constraints, with no further assumptions. We explore the relationship between the minimal representation problem and a certain set covering problem of Boneh. This provides a framework that shows the connection between minimal representations, irreducible infeasible systems, minimal infeasibility sets, as well as other attributes of the preprocessing of mathematical programs. The framework facilitates the development of preprocessing algorithms for a variety of mathematical programs. As some such algorithms require random sampling, we present results to identify those sets of constraints for which all information can be sampled with nonzero probability.

The term automated reasoning (first introduced in 1980) accurately describes the objective of the field, the automation of logical reasoning. This article introduces scientists to the field and then briefly describes the papers found in this special issue.

Contradiction separation based deduction is a key generalized inference rule of binary resolution, and has unique ability for automated theorem proving. Different inference rules need different proof searching strategies. This paper proposes two methods to avoid the repeated deductions and redundant clauses generated in the contradiction separation based deduction, that is, an improved clauses and literals weighted based method, and a redundant clauses prejudging and backtracking strategy. This work provides fundamental methods for contradiction separation based deduction on practical implementation.

The dominance of a reductionist approach in studies of managerial science has confined attention of researchers to the coarse aspects of the organization and its regularity. The method of analysis and solution of the problem has been to cancel interference generating unpredictability. The manager has been considered a major player in decision-making models based on the relationship between computational 'facts'. The separation between the complexity of events and management skills has become increasingly wide. It is urgent to rethink theories and managerial skills that may consider human actions as carriers of meanings, the organizations as emergent relationships based on 'values' and organizational change as a permanent process of development and evolution of personal know-how. Our contribution to the role of redundancy is part of the mainstream studies of organizational change best practices. Our view is that change creativity is a property of 'relational activity' and that it is necessary that management is able to acquire those 'subtle skills', both in studies and in practice, to be a 'co-generator of organizational values and well-being'.

For the large cost, low data availability in the condition of multi-node storage and poor capacity of intrusion tolerance of traditional disaster recovery which is based on simple copy, this paper put forward a distributed disaster recovery scheme based on raptor codes. This article introduces the principle of raptor codes, and analyses its coding advantages, and gives a comparative analysis between this solution and traditional solutions through the aspects of redundancy, data availability and capacity of intrusion tolerance. The results show that the distributed disaster recovery solution based on raptor codes can achieve higher data availability as well as better intrusion tolerance capabilities in the premise of lower redundancy.