Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

Filter by
Sorted by
Tagged with
6 votes
2 answers

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 ...
Mark's user avatar
  • 373
11 votes
1 answer

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 ...
TCSGrad's user avatar
  • 592
7 votes
1 answer

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,...
user2346's user avatar
  • 441
4 votes
1 answer

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 ...
Mohammad Al-Turkistany's user avatar
22 votes
1 answer

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,...
Vor's user avatar
  • 12.4k
20 votes
1 answer

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 ...
Juho's user avatar
  • 22.5k
30 votes
3 answers

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 ...
Artem Kaznatcheev's user avatar
20 votes
1 answer

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 ...
Adeiln's user avatar
  • 303
20 votes
1 answer

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.
jkjk's user avatar
  • 301

10 11 12 13