The problem of simplifying logical expressions

1959 ◽  
Vol 24 (1) ◽  
pp. 17-19 ◽  
Author(s):  
B. Dunham ◽  
R. Fridshal
Keyword(s):  
Normal Form ◽  
Simplification Techniques

By quite elementary means, one can find “large” examples difficult, if not (for practical purposes) impossible, to be managed by that host of methods, after Quine, for minimizing expressions in alternational normal form. Because the workability rather than existence of an algorithm for minimizing logical formulae is generally critical, it may be pertinent to outline briefly the derivation of these “large” examples. Some more general insight may also be gained about simplification techniques.

Chapter 9. Preprocessing in SAT Solving

2021 ◽  
Author(s):  
Armin Biere ◽  
Matti Järvisalo ◽  
Benjamin Kiesl
Keyword(s):  
Normal Form ◽  
Conjunctive Normal Form ◽  
Boolean Satisfiability ◽  
Sat Solving ◽  
Speed Up ◽  
Sat Solver ◽  
Main Ideas ◽  
Simplification Techniques

Preprocessing has become a key component of the Boolean satisfiability (SAT) solving workflow. In practice, preprocessing is situated between the encoding phase and the solving phase, with the aim of decreasing the total solving time by applying efficient simplification techniques on SAT instances to speed up the search subsequently performed by a SAT solver. In this chapter, we overview key preprocessing techniques proposed in the literature. While the main focus is on techniques applicable to formulas in conjunctive normal form (CNF), we also selectively cover main ideas for preprocessing structural and higher-level SAT instance representations.

scholarly journals Clause Elimination for SAT and QSAT

2015 ◽  
Vol 53 ◽  
pp. 127-168 ◽  
Author(s):  
Marijn Heule ◽  
Matti Järvisalo ◽  
Florian Lonsing ◽  
Martina Seidl ◽  
Armin Biere
Keyword(s):  
Normal Form ◽  
Real World ◽  
Practical Importance ◽  
Empirical Evaluation ◽  
Conjunctive Normal Form ◽  
Boolean Satisfiability ◽  
Practical Applications ◽  
Logical Equivalence ◽  
Hard Problems ◽  
Simplification Techniques

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of various computationally hard problems can be efficiently solved. This success has been achieved through several breakthroughs in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for prenex conjunctive normal form (PCNF) for QSAT---the standard input formats of SAT and QSAT solvers---have recently proven very effective in increasing solver efficiency when applied before (i.e., in preprocessing) or during (i.e., in inprocessing) satisfiability search. In this article, we develop and analyze clause elimination procedures for pre- and inprocessing. Clause elimination procedures form a family of (P)CNF formula simplification techniques which remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining the satisfiability status of the formulas. Extending known procedures such as tautology, subsumption, and blocked clause elimination, we introduce novel elimination procedures based on asymmetric variants of these techniques, and also develop a novel family of so-called covered clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. We analyze the considered clause elimination procedures from various perspectives. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to reconstruct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important for practical applications for the procedures. Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving.

Closing the GAP—A 5Å Scanning Microscope

1969 ◽  
Vol 27 ◽  
pp. 6-7
Author(s):  
A. V. Crewe
Keyword(s):  
Normal Form ◽  
The Other ◽  
Resolving Power ◽  
Scanning Microscope ◽  
Conventional Microscope ◽  
Other Hand ◽  
Closing The Gap ◽  
Thermal Sources ◽  
Better Than ◽  
Transmission Microscope

We have become accustomed to differentiating between the scanning microscope and the conventional transmission microscope according to the resolving power which the two instruments offer. The conventional microscope is capable of a point resolution of a few angstroms and line resolutions of periodic objects of about 1Å. On the other hand, the scanning microscope, in its normal form, is not ordinarily capable of a point resolution better than 100Å. Upon examining reasons for the 100Å limitation, it becomes clear that this is based more on tradition than reason, and in particular, it is a condition imposed upon the microscope by adherence to thermal sources of electrons.

A 3D Field Expression in Multilayered Structures using Jordan Normal Form

2012 ◽  
Vol 132 (8) ◽  
pp. 698-699 ◽  
Author(s):  
Hideaki Wakabayashi ◽  
Jiro Yamakita
Keyword(s):  
Normal Form ◽  
Jordan Normal Form ◽  
Multilayered Structures

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.

Analysis of a 2DOF Nonlinear Mechanical System Using the Normal Form Method

2019 ◽  
Author(s):  
David Julian Gonzalez Maldonado ◽  
Peter Hagedorn ◽  
Thiago Ritto ◽  
Rubens Sampaio ◽  
Artem Karev
Keyword(s):  
Normal Form ◽  
Mechanical System ◽  
Nonlinear Mechanical ◽  
Nonlinear Mechanical System ◽  
Normal Form Method

Normal form method in search for periodic solutions of ordinary differential equations. Case of the fourth order

2018 ◽  
pp. 24-34
Author(s):  
V. F. Edneral ◽  
O. D. Timofeevskaya
Keyword(s):  
Normal Form ◽  
Differential Equations ◽  
Ordinary Differential Equations ◽  
Periodic Solutions ◽  
Fourth Order ◽  
Numerical Solutions ◽  
Numerical Calculations ◽  
Computational Time ◽  
Resonant Normal Form ◽  
Normal Form Method

Introduction:The method of resonant normal form is based on reducing a system of nonlinear ordinary differential equations to a simpler form, easier to explore. Moreover, for a number of autonomous nonlinear problems, it is possible to obtain explicit formulas which approximate numerical calculations of families of their periodic solutions. Replacing numerical calculations with their precalculated formulas leads to significant savings in computational time. Similar calculations were made earlier, but their accuracy was insufficient, and their complexity was very high.Purpose:Application of the resonant normal form method and a software package developed for these purposes to fourth-order systems in order to increase the calculation speed.Results:It has been shown that with the help of a single algorithm it is possible to study equations of high orders (4th and higher). Comparing the tabulation of the obtained formulas with the numerical solutions of the corresponding equations shows good quantitative agreement. Moreover, the speed of calculation by prepared approximating formulas is orders of magnitude greater than the numerical calculation speed. The obtained approximations can also be successfully applied to unstable solutions. For example, in the Henon — Heyles system, periodic solutions are surrounded by chaotic solutions and, when numerically integrated, the algorithms are often unstable on them.Practical relevance:The developed approach can be used in the simulation of physical and biological systems.

The Study of State Simplification Techniques Based on Sensitive Position Identification

2014 ◽  
Vol 35 (3) ◽  
pp. 742-748
Author(s):  
Hong-bo Gao ◽  
Qing-bao Li ◽  
Wei Wang ◽  
Yu Zhu
Keyword(s):  
Simplification Techniques

The Logic of Normal-Form Games

2015 ◽  
Author(s):  
Gabriel Frahm
Keyword(s):  
Normal Form ◽  
Normal Form Games
Sign in / Sign up

Export Citation Format

Share Document