# Questions tagged [satisfiability]

For questions on the subject of "satisfiability", that is, whether there exists an interpretation/model in which a given (logical) formula is true.

194 questions
55 views

### Is there an instance 3-SAT on which this algorithm fails?

I'm not sure on how to express that in a very formal and absolutly correct way so I hope it is still understandable. I have found this algorithm and been struggling for a while proving it does or ...
33 views

### Using the reduction of 3-SAT to 3-COLOR, explain why complexity proofs by reduction work.

I'm reading about the proof that 3-COLOR is in NP-Hard, by reduction of 3-SAT to 3-COLOR (as listed here for example: http://cs.bme.hu/thalg/3sat-to-3col.pdf). And here's a passage from Wikipedia, ...
14 views

21 views

### satisfying boolean n variable DNF formula

I have an n variable boolean DNF formula and an input set,z consisting of n-tuples. Each tuple consists of truth/false assignment to n variable. the number of tuples in Z is not fixed, obviously <= ...
43 views

### Is there a standard quantifier notation for an exact number of true values?

When working with SAT Solvers, I need to write quantifiers that give the total number of true values. The usual quantitiers $\forall$ and $\exists$ do not suffice. Is there a standard notation for ...
16 views

### How would I reduce the Minimum Vertex Cover problem to a Weighted MAX SAT problem?

I am currently trying to solve the Minimum Vertex Cover problem via a Weighted MAX SAT solver, but I am stuck with the model. The transformation to a simple SAT is straightforward since every node can ...
42 views

### how to convert linear equation to cnf

I'm working on reduction from binary puzzle problem into sat. one of the game's rule is that in each row/column numbers of 1s equals to numbers of 0. I found a solution but it's exponential. Therefore,...
27 views

### What is the fastest, free Weighted SAT solver?

I want to solve the minimum vertex cover problem by solving and equivalent SAT instance. I tried several solvers, but I didn't find any solver which does weighted SAT. Do you know of any free SAT ...
84 views

### Eigenvalues and BIBO stability

Could someone please explain to me the relationship between eigenvalues of a system matrix A and BIBO stability? I've studied control engineering, and for example in modern control, we say that a ...
106 views

### Compactness Theorem for Propositional Logic

Here is the compactness theorem: If every finite subset of $\Phi$ is satisfiable, then $\Phi$ is satisfiable. Is the contrapositive the following? If $\Phi$ is unsatisfiable (tautologically ...