Chapter 2. CNF Encodings

2021 ◽  
Author(s):  
Steven Prestwich
Keyword(s):  
Normal Form ◽  
Case Studies ◽  
Search Algorithm ◽  
Empirical Work ◽  
Combinatorial Problem ◽  
Conjunctive Normal Form ◽  
Search Algorithms ◽  
File Format ◽  
Sources Of Error ◽  
Algorithm Implementation

Before a combinatorial problem can be solved by current SAT methods, it must usually be encoded in conjunctive normal form, which facilitates algorithm implementation and allows a common file format for problems. Unfortunately there are several ways of encoding most problems and few guidelines on how to choose among them, yet the choice of encoding can be as important as the choice of search algorithm. This chapter reviews theoretical and empirical work on encoding methods, including the use of Tseitin encodings, the encoding of extensional and intensional constraints, the interaction between encodings and search algorithms, and some common sources of error. Case studies are used for illustration.

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.

Rapid Search Algorithms of Local Registering Based on Decimal Tree

2013 ◽  
Vol 325-326 ◽  
pp. 1535-1538
Author(s):  
Zhen Hua Xia
Keyword(s):  
Search Algorithm ◽  
String Matching ◽  
Search Algorithms ◽  
Phone Number ◽  
Low Efficiency ◽  
Algorithm Implementation

In order to overcome the low efficiency of the database-based algorithm and the string-matching based algorithm in searching phone number, the two-level search algorithm by combining a decimal tree with a local registering table is proposed in this paper. The algorithm implementation is introduced in detail, and the experiments show that the decimal tree based algorithm is faster than the database-based algorithm and the string-matching based algorithm, especially much faster in the case of huge traffic.

On Starting Population Selection for GSAT

2013 ◽  
Vol 365-366 ◽  
pp. 190-193 ◽  
Author(s):  
Anna Gorbenko ◽  
Vladimir Popov
Keyword(s):  
Normal Form ◽  
Normal Forms ◽  
Search Algorithm ◽  
Conjunctive Normal Form ◽  
Random Functions ◽  
Population Selection ◽  
Selection For ◽  
Artificial Physics

GSAT is a well-known satisfiability search algorithm for conjunctive normal forms. GSAT uses some random functions. One of such functions is a function of starting population of truth assignments for the variables of conjunctive normal form. In this paper, we consider a method of artificial physics optimization for computing a function of starting population.

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 Circumspect descent prevails in solving random constraint satisfaction problems

2008 ◽  
Vol 105 (40) ◽  
pp. 15253-15257 ◽  
Author(s):  
Mikko Alava ◽  
John Ardelius ◽  
Erik Aurell ◽  
Petteri Kaski ◽  
Supriya Krishnamurthy ◽  
...  
Keyword(s):  
Local Search ◽  
Linear Time ◽  
Search Algorithm ◽  
Solution Space ◽  
Search Algorithms ◽  
Constraint Satisfaction Problems ◽  
Problem Instance ◽  
Stochastic Local Search ◽  
Local Search Algorithms ◽  
Local Energy Minimum

We study the performance of stochastic local search algorithms for random instances of the K-satisfiability (K-SAT) problem. We present a stochastic local search algorithm, ChainSAT, which moves in the energy landscape of a problem instance by never going upwards in energy. ChainSAT is a focused algorithm in the sense that it focuses on variables occurring in unsatisfied clauses. We show by extensive numerical investigations that ChainSAT and other focused algorithms solve large K-SAT instances almost surely in linear time, up to high clause-to-variable ratios α; for example, for K = 4 we observe linear-time performance well beyond the recently postulated clustering and condensation transitions in the solution space. The performance of ChainSAT is a surprise given that by design the algorithm gets trapped into the first local energy minimum it encounters, yet no such minima are encountered. We also study the geometry of the solution space as accessed by stochastic local search algorithms.

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 Finding A Small Vertex Cover in Massive Sparse Graphs: Construct, Local Search, and Preprocess

2017 ◽  
Vol 59 ◽  
pp. 463-494 ◽  
Author(s):  
Shaowei Cai ◽  
Jinkun Lin ◽  
Chuan Luo
Keyword(s):  
Local Search ◽  
Real World ◽  
Large Scale ◽  
Heuristic Algorithms ◽  
Search Algorithm ◽  
Vertex Cover ◽  
Search Algorithms ◽  
Theory And Practice ◽  
Sparse Graphs ◽  
Massive Graphs

The problem of finding a minimum vertex cover (MinVC) in a graph is a well known NP-hard combinatorial optimization problem of great importance in theory and practice. Due to its NP-hardness, there has been much interest in developing heuristic algorithms for finding a small vertex cover in reasonable time. Previously, heuristic algorithms for MinVC have focused on solving graphs of relatively small size, and they are not suitable for solving massive graphs as they usually have high-complexity heuristics. This paper explores techniques for solving MinVC in very large scale real-world graphs, including a construction algorithm, a local search algorithm and a preprocessing algorithm. Both the construction and search algorithms are based on low-complexity heuristics, and we combine them to develop a heuristic algorithm for MinVC called FastVC. Experimental results on a broad range of real-world massive graphs show that, our algorithms are very fast and have better performance than previous heuristic algorithms for MinVC. We also develop a preprocessing algorithm to simplify graphs for MinVC algorithms. By applying the preprocessing algorithm to local search algorithms, we obtain two efficient MinVC solvers called NuMVC2+p and FastVC2+p, which show further improvement on the massive graphs.

scholarly journals 7-Score Function for Assessing the Strength of Association Rules Applied for Construction Risk Quantifying

2022 ◽  
Vol 12 (2) ◽  
pp. 844
Author(s):  
Hubert Anysz ◽  
Jerzy Rosłon ◽  
Andrzej Foremny
Keyword(s):  
Association Analysis ◽  
Search Algorithm ◽  
Construction Project ◽  
Score Function ◽  
Road Construction ◽  
Combinatorial Problem ◽  
Macroeconomic Factors ◽  
Project Completion ◽  
Expert Opinions ◽  
Construction Risk

There are several factors influencing the time of construction project execution. The properties of the planned structure, the details of an order, and macroeconomic factors affect the project completion time. Every construction project is unique, but the data collected from previously completed projects help to plan the new one. The association analysis is a suitable tool for uncovering the rules—showing the influence of some factors appearing simultaneously. The input data to the association analysis must be preprocessed—every feature influencing the duration of the project must be divided into ranges. The number of features and the number of ranges (for each feature) create a very complicated combinatorial problem. The authors applied a metaheuristic tabu search algorithm to find the acceptable thresholds in the association analysis, increasing the strength of the rules found. The increase in the strength of the rules can help clients to avoid unfavorable sets of features, which in the past—with high confidence—significantly delayed projects. The new 7-score method can be used in various industries. This article shows its application to reduce the risk of a road construction contract delay. Importantly, the method is not based on expert opinions, but on historical data.

scholarly journals The Comparison of Docking Search Algorithms and Scoring Functions

2017 ◽  
pp. 820-849
Author(s):  
Marjana Novič ◽  
Tjaša Tibaut ◽  
Marko Anderluh ◽  
Jure Borišek ◽  
Tihomir Tomašič
Keyword(s):  
Organic Chemistry ◽  
Molecular Docking ◽  
Case Studies ◽  
Experimental Work ◽  
Cathepsin K ◽  
Docking Studies ◽  
Search Algorithms ◽  
Scoring Functions ◽  
Basic Information

This chapter, composed of two parts, firstly provides molecular docking overview and secondly two molecular docking case studies are described. In overview, basic information about molecular docking are presented such as description of search algorithms and scoring functions applied in various docking programs. Brief description of methods utilized in some of the most popular docking programs also applied in our experimental work is provided. AutoDock, CDOCKER, GOLD, FlexX and FRED were used for docking studies of the DC-SIGN protein, while GOLD was further used for docking studies of cathepsin K protein. Methods and results of our studies with their contribution to science and medicine are presented. Content of the chapter is therefore appropriate for public of Medicinal and Organic Chemistry as an overview of docking studies, and also for Computational Chemists at the beginning of their work as the introduction to application of molecular docking programs.

The Comparison of Docking Search Algorithms and Scoring Functions

2016 ◽  
pp. 99-127 ◽  
Author(s):  
Marjana Novič ◽  
Tjaša Tibaut ◽  
Marko Anderluh ◽  
Jure Borišek ◽  
Tihomir Tomašič
Keyword(s):  
Organic Chemistry ◽  
Molecular Docking ◽  
Case Studies ◽  
Experimental Work ◽  
Cathepsin K ◽  
Docking Studies ◽  
Search Algorithms ◽  
Scoring Functions ◽  
Basic Information

This chapter, composed of two parts, firstly provides molecular docking overview and secondly two molecular docking case studies are described. In overview, basic information about molecular docking are presented such as description of search algorithms and scoring functions applied in various docking programs. Brief description of methods utilized in some of the most popular docking programs also applied in our experimental work is provided. AutoDock, CDOCKER, GOLD, FlexX and FRED were used for docking studies of the DC-SIGN protein, while GOLD was further used for docking studies of cathepsin K protein. Methods and results of our studies with their contribution to science and medicine are presented. Content of the chapter is therefore appropriate for public of Medicinal and Organic Chemistry as an overview of docking studies, and also for Computational Chemists at the beginning of their work as the introduction to application of molecular docking programs.

Sign in / Sign up

Export Citation Format

Share Document