Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
659
questions
6
votes
2
answers
7k
views
Forward checking vs arc consistency on 3-SAT
If I were to let the variables be the propositions and, constraint be all clauses being satisfied, which technique would be more effective in solving 3-SAT? Forward checking or arc consistency? From ...
- 373
11
votes
1
answer
9k
views
How to prove that a constrained version of 3SAT in which no literal can occur more than once, is solvable in polynomial time?
I'm trying to work out an assignment (taken from the book Algorithms - by S. Dasgupta, C.H. Papadimitriou, and U.V. Vazirani, Chap 8, problem 8.6a), and I'm paraphrasing what it states:
Given that ...
- 592
7
votes
1
answer
15k
views
how do you prove that SAT is NP-complete?
As it is, how do you prove that SAT is NP-complete?
I know what it means by NP-complete, so I do not need an explanation on that.
What I want to know is how do you know that one problem, such as SAT,...
- 441
4
votes
1
answer
2k
views
Complexity of 3SAT variants
This question is motivated by my answer to another question in which I stated the fact that both Betweeness and Non-Betweeness problems are $NP$-complete. In the former problem there is a total order ...
- 4,417
22
votes
1
answer
2k
views
Classification of intractable/tractable satisfiability problem variants
Recently I found in a paper [1] a special symmetric version of SAT called the 2/2/4-SAT. But there are many $\text{NP}$-complete variants out there, for example: MONOTONE NAE-3SAT, MONOTONE 1-IN-3-SAT,...
- 12.4k
20
votes
1
answer
952
views
Supporting data structures for SAT local search
WalkSAT and GSAT are well-known and simple local search algorithms for solving the Boolean satisfiability problem. The pseudocode for the GSAT algorithm is copied from the question Implementing the ...
- 22.5k
30
votes
3
answers
1k
views
Measuring the difficulty of SAT instances
Given an instance of SAT, I would like to be able to estimate how difficult it will be to solve the instance.
One way is to run existing solvers, but that kind of defeats the purpose of estimating ...
- 4,812
20
votes
1
answer
3k
views
Implementing the GSAT algorithm - How to select which literal to flip?
The GSAT algorithm is, for the most part, straight forward: You get a formula in conjunctive normal form and flip the literals of the clauses until you find a solution that satisfies the formula or ...
- 303
20
votes
1
answer
4k
views
Proving that the conversion from CNF to DNF is NP-Hard
How can I prove that the conversion from CNF to DNF is NP-Hard?
I'm not asking for an answer, just some suggestions about how to go about proving it.
- 301