Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userSAT for pedestrians
271
0
0.0
(
0
)
Added by
Bernd Schuh
Publication date
2014
fields
Informatics Engineering
and research's language is
English
Authors
Bernd R. Schuh
Ask ChatGPT about the research
No Arabic abstract
The aim of this short note is mainly pedagogical. It summarizes some knowledge about Boolean satisfiability (SAT) and the P=NP? problem in an elementary mathematical language. A convenient scheme to visualize and manipulate CNF formulae is introduced. Also some results like the formulae for the number of unsatisfied clauses and the number of solutions might be unknown.
rate research
Read More
For random CNF formulae with m clauses, n variables and an unrestricted number of literals per clause the transition from high to low satisfiability can be determined exactly for large n. The critical density m/n turns out to be strongly n-dependent, ccr = ln(2)/(1-p)^^n, where pn is the mean number of positive literals per clause.This is in contrast to restricted random SAT problems (random K-SAT), where the critical ratio m/n is a constant. All transition lines are calculated by the second moment method applied to the number of solutions N of a formula. In contrast to random K-SAT, the method does not fail for the unrestricted model, because long range interactions between solutions are not cut off by disorder.
A heuristic model procedure for determining satisfiability of CNF-formulae is set up and described by nonlinear recursion relations for m (number of clauses), n (number of variables) and clause filling k. The system mimicked by the recursion undergoes a sharp transition from bounded running times (easy) to uncontrolled runaway behaviour (hard). Thus the parameter space turns out to be separated into regions with qualitatively different efficiency of the model procedure. The transition results from a competition of exponential blow up by branching versus growing number of orthogonal clauses.
Limits on the number of satisfying assignments for CNS instances with n variables and m clauses are derived from various inequalities. Some bounds can be calculated in polynomial time, sharper bounds demand information about the distribution of the number of unsatisfied clauses. Quite generally, the number of satisfying assignments involve variance and mean of this distribution. For large formulae, m>>1, bounds vary with 2**n/n, so they may be of use only for instances with a large number of satisfying assignments.
We present a (full) derandomization of HSSW algorithm for 3-SAT, proposed by Hofmeister, Schoning, Schuler, and Watanabe in [STACS02]. Thereby, we obtain an O(1.3303^n)-time deterministic algorithm for 3-SAT, which is currently fastest.
A generalized 1-in-3SAT problem is defined and found to be in complexity class P when restricted to a certain subset of CNF expressions. In particular, 1-in-kSAT with no restrictions on the number of literals per clause can be decided in polynomial time when restricted to exact READ-3 formulas with equal number of clauses (m) and variables (n), and no pure literals. Also individual instances can be checked for easiness with respect to a given SAT problem. By identifying whole classes of formulas as being solvable efficiently the approach might be of interest also in the complementary search for hard instances.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
