scholarly journals A Structural Entropy Measurement Principle of Propositional Formulas in Conjunctive Normal Form

Entropy ◽  
2021 ◽  
Vol 23 (3) ◽  
pp. 303
Author(s):  
Zaijun Zhang ◽  
Daoyun Xu ◽  
Jincheng Zhou
Keyword(s):  
Normal Form ◽  
Local Search ◽  
Structural Properties ◽  
Structural Characteristics ◽  
Complex Structure ◽  
Solution Process ◽  
Conjunctive Normal Form ◽  
Experimental Results ◽  
Entropy Measurement ◽  
Structural Entropy

The satisfiability (SAT) problem is a core problem in computer science. Existing studies have shown that most industrial SAT instances can be effectively solved by modern SAT solvers while random SAT instances cannot. It is believed that the structural characteristics of different SAT formula classes are the reasons behind this difference. In this paper, we study the structural properties of propositional formulas in conjunctive normal form (CNF) by the principle of structural entropy of formulas. First, we used structural entropy to measure the complex structure of a formula and found that the difficulty solving the formula is related to the structural entropy of the formula. The smaller the compressing information of a formula, the more difficult it is to solve the formula. Secondly, we proposed a λ-approximation strategy to approximate the structural entropy of large formulas. The experimental results showed that the proposed strategy can effectively approximate the structural entropy of the original formula and that the approximation ratio is more than 92%. Finally, we analyzed the structural properties of a formula in the solution process and found that a local search solver tends to select variables in different communities to perform the next round of searches during a search and that the structural entropy of a variable affects the probability of the variable being flipped. By using these conclusions, we also proposed an initial candidate solution generation strategy for a local search for SAT, and the experimental results showed that this strategy effectively improves the performance of the solvers CCAsat and Sparrow2011 when incorporated into these two solvers.

scholarly journals Extended Conjunctive Normal Form and An Efficient Algorithm for Cardinality Constraints

2020 ◽  
Author(s):  
Zhendong Lei ◽  
Shaowei Cai ◽  
Chuan Luo
Keyword(s):  
Normal Form ◽  
Local Search ◽  
State Of The Art ◽  
Scoring Function ◽  
Conjunctive Normal Form ◽  
Discrete Tomography ◽  
Cardinality Constraint ◽  
Cardinality Constraints ◽  
Important Constraint ◽  
Unit Propagation

Satisfiability (SAT) and Maximum Satisfiability (MaxSAT) are two basic and important constraint problems with many important applications. SAT and MaxSAT are expressed in CNF, which is difficult to deal with cardinality constraints. In this paper, we introduce Extended Conjunctive Normal Form (ECNF), which expresses cardinality constraints straightforward and does not need auxiliary variables or clauses. Then, we develop a simple and efficient local search solver LS-ECNF with a well designed scoring function under ECNF. We also develop a generalized Unit Propagation (UP) based algorithm to generate the initial solution for local search. We encode instances from Nurse Rostering and Discrete Tomography Problems into CNF with three different cardinality constraint encodings and ECNF respectively. Experimental results show that LS-ECNF has much better performance than state of the art MaxSAT, SAT, Pseudo-Boolean and ILP solvers, which indicates solving cardinality constraints with ECNF is promising.

scholarly journals A new structural entropy measurement of networks based on the nonextensive statistical mechanics and hub repulsion

2021 ◽  
Vol 18 (6) ◽  
pp. 9253-9263
Author(s):  
Fu Tan ◽  
◽  
Bing Wang ◽  
Daijun Wei
Keyword(s):  
Statistical Mechanics ◽  
Complex Networks ◽  
Structural Properties ◽  
Complex Network ◽  
Repulsive Force ◽  
Nonextensive Statistical Mechanics ◽  
Entropy Measurement ◽  
Structural Entropy ◽  
Degree Structure ◽  
The Difference

<abstract><p>The structure properties of complex networks are an open issue. As the most important parameter to describe the structural properties of the complex network, the structure entropy has attracted much attention. Recently, the researchers note that hub repulsion plays an role in structural entropy. In this paper, the repulsion between nodes in complex networks is simulated when calculating the structure entropy of the complex network. Coulomb's law is used to quantitatively express the repulsive force between two nodes of the complex network, and a new structural entropy based on the Tsallis nonextensive statistical mechanics is proposed. The new structure entropy synthesizes the influence of repulsive force and betweenness. We study several construction networks and some real complex networks, the results show that the proposed structure entropy can describe the structural properties of complex networks more reasonably. In particular, the new structural entropy has better discrimination in describing the complexity of the irregular network. Because in the irregular network, the difference of the new structure entropy is larger than that of degree structure entropy, betweenness structure entropy and Zhang's structure entropy. It shows that the new method has better discrimination for irregular networks, and experiments on Graph, Centrality literature, US Aire lines and Yeast networks confirm this conclusion.</p></abstract>

METHODS OF REDUCING OF LARGE BOOLEAN FORMULAS REPRESENTED IN A CONJUNCTIVE NORMAL FORM FOR DETERMINING THEIR SATISFIABILITY

2020 ◽  
Author(s):  
N.I. Gdansky ◽  
◽  
A.A. Denisov ◽  
Keyword(s):  
Normal Form ◽  
Normal Forms ◽  
Conjunctive Normal Form ◽  
Boolean Formulas

The article explores the satisfiability of conjunctive normal forms used in modeling systems.The problems of CNF preprocessing are considered.The analysis of particular methods for reducing this formulas, which have polynomial input complexity is given.

scholarly journals DNA-Guided Assembly for Fibril Proteins

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 404
Author(s):  
Alexandru Amărioarei ◽  
Frankie Spencer ◽  
Gefry Barad ◽  
Ana-Maria Gheorghe ◽  
Corina Iţcuş ◽  
...  
Keyword(s):  
Computational Model ◽  
Structural Properties ◽  
Self Assembly ◽  
Structural Characteristics ◽  
Computational Modelling ◽  
Shape Reconstruction ◽  
Raw Material ◽  
Dna Assembly ◽  
Mesh Structure ◽  
Elementary Fibril

Current advances in computational modelling and simulation have led to the inclusion of computer scientists as partners in the process of engineering of new nanomaterials and nanodevices. This trend is now, more than ever, visible in the field of deoxyribonucleic acid (DNA)-based nanotechnology, as DNA’s intrinsic principle of self-assembly has been proven to be highly algorithmic and programmable. As a raw material, DNA is a rather unremarkable fabric. However, as a way to achieve patterns, dynamic behavior, or nano-shape reconstruction, DNA has been proven to be one of the most functional nanomaterials. It would thus be of great potential to pair up DNA’s highly functional assembly characteristics with the mechanic properties of other well-known bio-nanomaterials, such as graphene, cellulos, or fibroin. In the current study, we perform projections regarding the structural properties of a fibril mesh (or filter) for which assembly would be guided by the controlled aggregation of DNA scaffold subunits. The formation of such a 2D fibril mesh structure is ensured by the mechanistic assembly properties borrowed from the DNA assembly apparatus. For generating inexpensive pre-experimental assessments regarding the efficiency of various assembly strategies, we introduced in this study a computational model for the simulation of fibril mesh assembly dynamical systems. Our approach was based on providing solutions towards two main circumstances. First, we created a functional computational model that is restrictive enough to be able to numerically simulate the controlled aggregation of up to 1000s of elementary fibril elements yet rich enough to provide actionable insides on the structural characteristics for the generated assembly. Second, we used the provided numerical model in order to generate projections regarding effective ways of manipulating one of the the key structural properties of such generated filters, namely the average size of the openings (gaps) within these meshes, also known as the filter’s aperture. This work is a continuation of Amarioarei et al., 2018, where a preliminary version of this research was discussed.

scholarly journals A Multiple and Multi-Level Substructure Method for the Dynamics of Complex Structures

2021 ◽  
Vol 11 (12) ◽  
pp. 5570
Author(s):  
Binbin Wang ◽  
Jingze Liu ◽  
Zhifu Cao ◽  
Dahai Zhang ◽  
Dong Jiang
Keyword(s):  
Structural Characteristics ◽  
Complex Structure ◽  
Complex Structures ◽  
System Matrix ◽  
Substructure Method ◽  
Residual Structure ◽  
The Matrix ◽  
Multi Level ◽  
Fixed Interface ◽  
Selection Of

Based on the fixed interface component mode synthesis, a multiple and multi-level substructure method for the modeling of complex structures is proposed in this paper. Firstly, the residual structure is selected according to the structural characteristics of the assembled complex structure. Secondly, according to the assembly relationship, the parts assembled with the residual structure are divided into a group of substructures, which are named the first-level substructure, the parts assembled with the first-level substructure are divided into a second-level substructure, and consequently the multi-level substructure model is established. Next, the substructures are dynamically condensed and assembled on the boundary of the residual structure. Finally, the substructure system matrix, which is replicated from the matrix of repeated physical geometry, is obtained by preserving the main modes and the constrained modes and the system matrix of the last level of the substructure is assembled to the upper level of the substructure, one level up, until it is assembled in the residual structure. In this paper, an assembly structure with three panels and a gear box is adopted to verify the method by simulation and a rotor is used to experimentally verify the method. The results show that the proposed multiple and multi-level substructure modeling method is not unique to the selection of residual structures, and different classification methods do not affect the calculation accuracy. The selection of 50% external nodes can further improve the analysis efficiency while ensuring the calculation accuracy.

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

scholarly journals Many-Objective Genetic Programming for Job-Shop Scheduling

2021 ◽  
Author(s):  
◽  
Atiya Masood
Keyword(s):  
Local Search ◽  
Pareto Front ◽  
Job Shop ◽  
Optimization Problems ◽  
Reference Points ◽  
Experimental Results ◽  
Dispatching Rules ◽  
Model Driven ◽  
Conflicting Objectives ◽  
Mean Function

<p>The Job Shop Scheduling (JSS) problem is considered to be a challenging one due to practical requirements such as multiple objectives and the complexity of production flows. JSS has received great attention because of its broad applicability in real-world situations. One of the prominent solutions approaches to handling JSS problems is to design effective dispatching rules. Dispatching rules are investigated broadly in both academic and industrial environments because they are easy to implement (by computers and shop floor operators) with a low computational cost. However, the manual development of dispatching rules is time-consuming and requires expert knowledge of the scheduling environment. The hyper-heuristic approach that uses genetic programming (GP) to solve JSS problems is known as GP-based hyper-heuristic (GP-HH). GP-HH is a very useful approach for discovering dispatching rules automatically.  Although it is technically simple to consider only a single objective optimization for JSS, it is now widely evidenced in the literature that JSS by nature presents several potentially conflicting objectives, including the maximal flowtime, mean flowtime, and mean tardiness. A few studies in the literature attempt to solve many-objective JSS with more than three objectives, but existing studies have some major limitations. First, many-objective JSS problems have been solved by multi-objective evolutionary algorithms (MOEAs). However, recent studies have suggested that the performance of conventional MOEAs is prone to the scalability challenge and degrades dramatically with many-objective optimization problems (MaOPs). Many-objective JSS using MOEAs inherit the same challenge as MaOPs. Thus, using MOEAs for many-objective JSS problems often fails to select quality dispatching rules. Second, although the reference points method is one of the most prominent and efficient methods for diversity maintenance in many-objective problems, it uses a uniform distribution of reference points which is only appropriate for a regular Pareto-front. However, JSS problems often have irregular Pareto-front and uniformly distributed reference points do not match well with the irregular Pareto-front. It results in many useless points during evolution. These useless points can significantly affect the performance of the reference points-based algorithms. They cannot help to enhance the solution diversity of evolved Pareto-front in many-objective JSS problems. Third, Pareto Local Search (PLS) is a prominent and effective local search method for handling multi-objective JSS optimization problems but the literature does not discover any existing studies which use PLS in GP-HH.  To address these limitations, this thesis's overall goal is to develop GP-HH approaches to evolving effective rules to handle many conflicting objectives simultaneously in JSS problems.  To achieve the first goal, this thesis proposes the first many-objective GP-HH method for JSS problems to find the Pareto-fronts of nondominated dispatching rules. Decision-makers can utilize this GP-HH method for selecting appropriate rules based on their preference over multiple conflicting objectives. This study combines GP with the fitness evaluation scheme of a many-objective reference points-based approach. The experimental results show that the proposed algorithm significantly outperforms MOEAs such as NSGA-II and SPEA2.  To achieve the second goal, this thesis proposes two adaptive reference point approaches (model-free and model-driven). In both approaches, the reference points are generated according to the distribution of the evolved dispatching rules. The model-free reference point adaptation approach is inspired by Particle Swarm Optimization (PSO). The model-driven approach constructs the density model and estimates the density of solutions from each defined sub-location in a whole objective space. Furthermore, the model-driven approach provides smoothness to the model by applying a Gaussian Process model and calculating the area under the mean function. The mean function area helps to find the required number of the reference points in each mean function. The experimental results demonstrate that both adaptive approaches are significantly better than several state-of-the-art MOEAs.  To achieve the third goal, the thesis proposes the first algorithm that combines GP as a global search with PLS as a local search in many-objective JSS. The proposed algorithm introduces an effective fitness-based selection strategy for selecting initial individuals for neighborhood exploration. It defines the GP's proper neighborhood structure and a new selection mechanism for selecting the effective dispatching rules during the local search. The experimental results on the JSS benchmark problem show that the newly proposed algorithm can significantly outperform its baseline algorithm (GP-NSGA-III).</p>

Chapter 13. Symmetry and Satisfiability

2021 ◽  
Author(s):  
Karem A. Sakallah
Keyword(s):  
Group Theory ◽  
Normal Form ◽  
Boolean Functions ◽  
Search Algorithm ◽  
Conjunctive Normal Form ◽  
Search Space ◽  
Decision Problems ◽  
Mathematical Language ◽  
Sat Solvers ◽  
Speed Up

Symmetry is at once a familiar concept (we recognize it when we see it!) and a profoundly deep mathematical subject. At its most basic, a symmetry is some transformation of an object that leaves the object (or some aspect of the object) unchanged. For example, a square can be transformed in eight different ways that leave it looking exactly the same: the identity “do-nothing” transformation, 3 rotations, and 4 mirror images (or reflections). In the context of decision problems, the presence of symmetries in a problem’s search space can frustrate the hunt for a solution by forcing a search algorithm to fruitlessly explore symmetric subspaces that do not contain solutions. Recognizing that such symmetries exist, we can direct a search algorithm to look for solutions only in non-symmetric parts of the search space. In many cases, this can lead to significant pruning of the search space and yield solutions to problems which are otherwise intractable. This chapter explores the symmetries of Boolean functions, particularly the symmetries of their conjunctive normal form (CNF) representations. Specifically, it examines what those symmetries are, how to model them using the mathematical language of group theory, how to derive them from a CNF formula, and how to utilize them to speed up CNF SAT solvers.

Sign in / Sign up

Export Citation Format

Share Document