The (Coarse) Fine-Grained Structure of NP-Hard SAT and CSP Problems

We study the fine-grained complexity of NP-complete satisfiability (SAT) problems and constraint satisfaction problems (CSPs) in the context of the strong exponential-time hypothesis (SETH) , showing non-trivial lower and upper bounds on the running time. Here, by a non-trivial lower bound for a problem SAT (Γ) (respectively CSP (Γ)) with constraint language Γ, we mean a value c 0 > 1 such that the problem cannot be solved in time O ( c n ) for any c < c 0 unless SETH is false, while a non-trivial upper bound is simply an algorithm for the problem running in time O ( c n ) for some c < 2. Such lower bounds have proven extremely elusive, and except for cases where c 0 =2 effectively no such previous bound was known. We achieve this by employing an algebraic framework, studying constraint languages Γ in terms of their algebraic properties. We uncover a powerful algebraic framework where a mild restriction on the allowed constraints offers a concise algebraic characterization. On the relational side we restrict ourselves to Boolean languages closed under variable negation and partial assignment, called sign-symmetric languages. On the algebraic side this results in a description via partial operations arising from system of identities, with a close connection to operations resulting in tractable CSPs, such as near unanimity operations and edge operations . Using this connection we construct improved algorithms for several interesting classes of sign-symmetric languages, and prove explicit lower bounds under SETH. Thus, we find the first example of an NP-complete SAT problem with a non-trivial algorithm which also admits a non-trivial lower bound under SETH. This suggests a dichotomy conjecture with a close connection to the CSP dichotomy theorem: an NP-complete SAT problem admits an improved algorithm if and only if it admits a non-trivial partial invariant of the above form.

P Systems with Evolutional Communication and Division Rules

A widely studied field in the framework of membrane computing is computational complexity theory. While some types of P systems are only capable of efficiently solving problems from the class P, adding one or more syntactic or semantic ingredients to these membrane systems can give them the ability to efficiently solve presumably intractable problems. These ingredients are called to form a frontier of efficiency, in the sense that passing from the first type of P systems to the second type leads to passing from non-efficiency to the presumed efficiency. In this work, a solution to the SAT problem, a well-known NP-complete problem, is obtained by means of a family of recognizer P systems with evolutional symport/antiport rules of length at most (2,1) and division rules where the environment plays a passive role; that is, P systems from CDEC^(2,1). This result is comparable to the one obtained in the tissue-like counterpart, and gives a glance of a parallelism and the non-evolutionary membrane systems with symport/antiport rules.

CNF-SAT modelling for banyan-type networks and its application for assessing the rearrangeability

A banyan-type network is a switching network, which is constructed by placing unit switches with two inputs and two outputs in s (s > 1) stages. In each stage, 2 n – 1 (n > 1) unit switches are aligned. Past studies conjecture that this network becomes rearrangeable when s ≥ 2n-1. Although a considerable number of theoretical analyses have been done, the rearrangeability of the banyan-type network with 2n – 1 or more stages is not completely proved. As a tool to assess the rearrangeability, this study presents a CNF-SAT (conjunctive normal form - satisfiability) modelling scheme for banyan-type networks. In the proposed scheme, the routing is formulated to a SAT problem represented in CNF. By feeding the problem to a SAT solver, it is found whether the problem is satisfiable or unsatisfiable. If the problem is unsatisfiable for a certain request, the network is not rearrangeable. By contrast, if the problem is satisfiable for any requests, the network is rearrangeable. This study applies the CNF-SAT modelling scheme to various configurations of 2n – 1 stage banyan-type networks. These networks are assessed for rearrangeability by solving the SAT problems. The proposed method will be helpful to conduct future theoretical studies on banyan-type networks.

A New Method for 3-Satisfiability Problem Solving Space Structure on Structural Entropy

Analyzing the solution space structure and evolution of 3satisfiability (3-SAT) problem is an important way to study the difficulty of the solving satisfiability (SAT) problem. However, there is no unified analysis model for the spatial structure and evolution of solutions under different constraint densities. The analysis of different phase transition points and solution regions is based on different metric analysis models. The solution space of 3-SAT problem is obtained by planting strategy and belief propagation. According to the distribution of the influence of frozen variables on the solution, a label propagation algorithm based on planting strategy is proposed, is used to find the solution cluster, and then the structure entropy is used to measure its structure information. The structure entropy analysis model of 3-SAT problem solution space is established, and the unified analysis framework of solution space evolution and satisfiability phase transition is given. The experimental results show that the model is effective and can accurately analyze the evolution process of solution space and satisfiability phase transition, and verify the accuracy of interference phase transition point threshold predicted by long-range frustration theory.

Resolvable Networks—A Graphical Tool for Representing and Solving SAT

In this paper, we introduce the notion of resolvable networks. A resolvable network is a digraph of subnetworks, where subnetworks may overlap, and the inner structure of subnetworks are not interesting from the viewpoint of the network. There are two special subnetworks, Source and Sink, with the following properties: there is no incoming edge to Source, and there is no outgoing edge from Sink. Any resolvable network can be represented by a satisfiability problem in Boolean logic (shortly, SAT problem), and any SAT problem can be represented by a resolvable network. Because of that, the resolution operation is valid also for resolvable networks. We can use resolution to find out or refine the inner structure of subnetworks. We give also a pessimistic and an optimistic interpretation of subnetworks. In the pessimistic case, we assume that inside a subnetwork, all communication possibilities are represented as part of the resolvable network. In the optimistic case, we assume that each subnetwork is strongly connected. We show that any SAT problem can be visualized using the pessimistic interpretation. We show that transitivity is very limited in the pessimistic interpretation, and in this case, transitivity corresponds to resolution of clauses. In the optimistic interpretation of subnetworks, we have transitivity without any further condition, but not all SAT problems can be represented in this case; however, any such network can be represented as a SAT problem. The newly introduced graphical concept allows to use terminology and tools from directed graphs in the field of SAT and also to give graphical representations of various concepts of satisfiability problems. A resolvable network is also a suitable data structure to study, for example, wireless sensor networks. The visualization power of resolvable networks is demonstrated on some pigeon hole SAT problems. Another important application field could be modeling the communication network of an information bank. Here, a subnetwork represents a dataset of a user which is secured by a proxy. Any communication should be done through the proxy, and this constraint can be checked using our model.

Satisfiability in Boolean Logic (SAT problem) is polynomial?

We find a polynomial algorithm to solve SAT problem in Boolean Logic

Satisfiability Checking of Strategy Logic with Simple Goals

In this paper, we introduce a new method of the satisfiability (SAT) checking for Simple-Goal Strategy Logic (SL[SG]), using symbolic Boolean model encoding and the SAT Modulo Monotonic Theories techniques, which was implemented into the tool SGSAT. To the best of our knowledge, this is the only tool solving the SAT problem for SL[SG]. Its applications include process synthesis, developing controllers as well as automatic planners in multi-agent scenarios.

The Phase Transition Analysis for the Random Regular Exact 2-(d,k)-SAT Problem

In a regular (d,k)-CNF formula, each clause has length k and each variable appears d times. A regular structure such as this is symmetric, and the satisfiability problem of this symmetric structure is called the (d,k)-SAT problem for short. The regular exact 2-(d,k)-SAT problem is that for a (d,k)-CNF formula F, if there is a truth assignment T, then exactly two literals of each clause in F are true. If the formula F contains only positive or negative literals, then there is a satisfiable assignment T with a size of 2n/k such that F is 2-exactly satisfiable. This paper introduces the (d,k)-SAT instance generation model, constructs the solution space, and employs the method of the first and second moments to present the phase transition point d* of the 2-(d,k)-SAT instance with only positive literals. When d<d*, the 2-(d,k)-SAT instance can be satisfied with high probability. When d>d*, the 2-(d,k)-SAT instance can not be satisfied with high probability. Finally, the verification results demonstrate that the theoretical results are consistent with the experimental results.