Git Repo: git@github.com:Wenling/DPLL-Algorithm.git
There are three satisfiability-preserving transformations in DP.
• The 1-literal rule
• The affirmative-negative rule
• The rule for eliminating atomic formulas
The first two steps reduce the total number of literals in the formula.
The last step reduces the number of variables in the formula.
By repeatedly applying these rules, eventually we obtain a formula containing an
empty clause, indicating unsatisfiability, or a formula with no clauses, indicating
satisfiability.
The DPLL algorithm replaces resolution with a splitting rule.
• Choose a propositional symbol p occuring in the formula.
• Let delta be the current set of clauses.
• Test the satisfiability of delta and {p}.
• If satisfiable, return true.
• Otherwise, return the result of testing delta and {¬p} for satisfiability.
Showing posts with label SAT. Show all posts
Showing posts with label SAT. Show all posts
4/25/2012
3/10/2012
SAT Solver
In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE.
SAT was the first known example of an NP-complete problem. That briefly means that there is no known algorithm that efficiently solves all instances of SAT, and it is generally believed (but not proven, see P versus NP problem) that no such algorithm can exist.
3-satisfiability is a special case of k-satisfiability (k-SAT) or simply satisfiability (SAT), when each clause contains exactly k = 3 literals.
3-SAT is NP-complete and it is used as a starting point for proving that other problems are also NP-hard. This is done by polynomial-time reduction from 3-SAT to the other problem.
EG. Subset sum problem
Assume that we are given some integers, such as {-7, -3, -2, 5, 8}, and we wish to know whether some of the integers can add up to zero. As the number of integers that we feed into the algorithm becomes larger, the number of subsets grows exponentially, and in fact the subset sum problem is NP-complete. An algorithm that verifies whether a given subset has sum zero is called verifier. A problem is said to be in NP if and only if there exists a verifier for the problem that executes in polynomial time.
SAT was the first known example of an NP-complete problem. That briefly means that there is no known algorithm that efficiently solves all instances of SAT, and it is generally believed (but not proven, see P versus NP problem) that no such algorithm can exist.
3-satisfiability is a special case of k-satisfiability (k-SAT) or simply satisfiability (SAT), when each clause contains exactly k = 3 literals.
3-SAT is NP-complete and it is used as a starting point for proving that other problems are also NP-hard. This is done by polynomial-time reduction from 3-SAT to the other problem.
EG. Subset sum problem
Assume that we are given some integers, such as {-7, -3, -2, 5, 8}, and we wish to know whether some of the integers can add up to zero. As the number of integers that we feed into the algorithm becomes larger, the number of subsets grows exponentially, and in fact the subset sum problem is NP-complete. An algorithm that verifies whether a given subset has sum zero is called verifier. A problem is said to be in NP if and only if there exists a verifier for the problem that executes in polynomial time.
Subscribe to:
Comments (Atom)