69
votes
What is the $3$-SAT problem?
There are a bunch of teddy bears A, B, C, D and so on that are red on one side and blue on the other! (You choose how to color them)
AND there are a bunch of 3 armed aliens with really long arms. ...
- 819
12
votes
Why does Skolemming not preserve validity?
When the existentials that are being removed in the process of Skolemization are not preceded y universals, you simply use a new constant for the respective variables.
As such, consider the formula:
...
- 98.1k
10
votes
Accepted
Why does Skolemming not preserve validity?
A sentence is valid if it is true in every interpretation of its logical language.
A sentence is satisfiable if it is true in some interpetation of its logical language.
Since Skolemization adds new ...
8
votes
Accepted
FOL - If two models agree on every sentence are they isomorphic?
Your intuition is exactly right - elementary equivalence (= satisfy the same first-order sentences) is not the same as isomorphism. Moreover, you're right that the place to look is cardinality ...
- 240k
7
votes
Accepted
There exists no zero-order or first-order theory for connected graphs
Assume you have a first-order theory $T$ in the language of graphs such that the models of $T$ are precisely the connected graphs. (The language of graphs has one two-place relation symbol $R,$ where $...
- 9,387
6
votes
Accepted
How exactly does a Max 2 Sat reduce to a 3 Sat?
First, the article is reducing 3SAT to Max2SAT (not Max2SAT to 3SAT).
In 3SAT, each clause has 3 variables and has the form $c_i=(l_1 \cup l_2 \cup l_3)$.
For each clause $c_i$, create the following ...
- 2,565
6
votes
Accepted
Tarski criterion fails? , $\Sigma_1$ formula,elementary substructure
Because your statement of the Tarski-Vaught test is wrong. Here's what it really says:
Let $M$ be a substructure of $N$. Then $M\preceq N$ if and only if for every first-order formula $\psi(x,\...
- 73.8k
6
votes
Accepted
Is Boolean Satisfiability Problem for CNF is NP? What about DNF?
Yes, for DNF it is trivial ... but note that converting a CNF into DNF is very costly: you have to do a general distribution of all terms over all terms. For example, suppose you have a CNF with $5$ ...
- 98.1k
6
votes
Accepted
Is XOR-SAT + $2$-SAT in P?
There is no polynomial-time procedure for deciding the satisfiability of 2-SAT + XOR-SAT unless P = NP. So, probably not. 2-SAT + XOR-SAT is easily proven NP-complete by direct polynomial reduction ...
- 1,851
5
votes
Why does Skolemming not preserve validity?
When you Skolemize, you drop the existential quantifier in front of $f$. Every structure that is a model of the original formula can be extended by providing an interpretation of $f$. Such an ...
- 7,646
5
votes
Accepted
What's the meaning of "$F \models \bot$" in propositional logic?
$F \models \bot$ means that there is no valuation $v$ that satisfies the formula $F$.
If $F \models \bot$, then it is vacuously true that every valuation that satisfies $F$ satisfies $G$ as well (...
- 16.4k
5
votes
Accepted
What symbol should be used to indicate that two propositions are consistent with each other?
I'm sorry to disappoint your expectations, but the widely used notation to say that two propositions $p$ and $q$ are consistent with each other is $p,q \not\vdash \bot$ or $\text{Con}(\{p,q\})$.
This ...
- 16.4k
5
votes
Accepted
Take a 3-SAT system and compute its symmetry group, what can we say? How does this group relate to satisfiability?
It seems to me that there are two reasonable notions of "symmetry group" here. I would call them "intensional" and "extensional". Let me make this precise.
Let $P$ be a ...
- 73.8k
4
votes
Accepted
How to prove tautology
First, suppose that $\Gamma \models F$. This means that for every interpretation $I$ such that $\phi[I]$ is true for all $\phi \in \Gamma$ we have that $F[I]$ is true. In other words, there is no ...
- 16.6k
4
votes
Accepted
Definition of a model?
See Resolution: the set $\phi$ of formulas can be read as a single formula in Conjunctive normal form, i.e. as
$(a \lor b) \land (a \lor c) \land (\lnot d \lor \lnot e \lor \lnot f)$.
An implicant ...
- 93k
4
votes
A formula is satisfiable under $I \iff |I|=1$?
If there is more than one constant symbol in the language, then this is not true. For example if $c$ and $d$ are constant symbols, then $A$ could be the sentence (with no free variables) $\lnot (c = d)...
- 73.8k
4
votes
Accepted
Compactness Theorem for Propositional Logic
The comment from @spaceisdarkgreen is correct, but maybe a little more explanation would help. The contrapositive of "if A then B" is "if it's not the case that B then it's not the case that A. In ...
- 70.7k
4
votes
Accepted
Is there a generally agreed upon definition of "satisfiability" for arbitrary logics?
To talk about "arbitrary logics" we need some kind of formalism describing what a logic is in the abstract. A very general definition would be
An abstract logic is a pair of sets $I$ and $S,$ and ...
- 56.7k
4
votes
Accepted
What is wrong with this definition of a truth predicate?
That's not actually an algorithm in the sense of a computable process: already, checking truth of $\Sigma_1$ sentences is not computable.
And if we switch to the language of, well, language, things ...
- 240k
4
votes
Is 3-SAT useful for anything practical?
I think your approach would be completely infeasible and I am sure that no such table exists. The good news is that SAT solvers using clever algorithms and heuristics are able to solve formulas ...
- 45.9k
4
votes
Accepted
Must we define $\mathcal A \models (\varphi \wedge \psi)$ using the word "and"?
Defining satisfaction like this isn't wrong, per se -- in fact there's arguably no real distinction between this and the usual way -- but it puts undue emphasis on the formalization of the metatheory.
...
- 56.7k
3
votes
Accepted
What is the definition of the complement of a decision problem?
A "decision problem" is usually defined to be a subset $P$ of some given set $L$ (which I will refer to as a "language"), whose elements can be represented in some agreed way as inputs to a Turing ...
- 45.9k
3
votes
Why is SAT the complement of TAUTOLOGY?
A formula $A$ is a tautology if it is true with every assignment.
A formula $A$ is satisfiable if there is at least an assignemnt $v$ such that $A$ is true for $v$.
If $A$ is true for the assignment $...
- 93k
3
votes
Accepted
Expressing 3SAT clause as a 2SAT formula
Suppose you have a representation of $x_1\lor x_2\lor x_3$ as 2CNF clauses, possibly involving with hidden variables. (This would "represent" the three-way disjunction in the sense that the 2CNF is ...
3
votes
Accepted
Contradiction in Davis–Putnam–Logemann–Loveland (DPLL) Method?!
Let $\Phi$ the initial set of four clauses as above.
Def 15. A pure literal is a literal $l$ that appears in at least one clause of $\Phi$ while $\lnot l$ doers not appear in any clause of $\Phi$.
...
- 93k
3
votes
In satisfiability, what is the difference between the empty clause and the empty clause set?
You can get an intuition why this is so by observing that:
A disjunction is true iff there exists a member which is true. In an empty disjunction (empty clause) there is no such member, so it is ...
- 31
3
votes
Accepted
How to prove that 3-CNF is satisfiable using Hall's marriage theorem?
You've already set the problem up, and the rest is a classic corollary of Hall's theorem:
Every $k$-regular bipartite graph has a perfect matching.
In case you are unfamiliar: here $k$-regular ...
- 6,201
3
votes
Accepted
First Order Logic - Logical Consequence and Paradox
When you derive the empty clause from a set of clauses that indeed means that that set of clauses is not satisfiable.
However, when you try to figure out whether some statement $\varphi$ follows from ...
- 98.1k
3
votes
Why doesn't implication graph work for 3SAT as it does for 2SAT?
It might be helpful to consider the related problem in resolution first. Briefly, if we consider 2-SAT, the clauses all contain only two literals, so the resolvent of those two clauses still has at ...
- 1,690
3
votes
Determining when Ax=b is consistent
Do the row reduction on the augmented matrix
$$
\left[\begin{array}{ccc|c}
1 & -3 &2 & b_1\\
-2 & 5 &-1 & b_2\\
3&-3 &-12 &b_3\end{array}
\right]
$$
instead.
- 33.1k
Only top scored, non community-wiki answers of a minimum length are eligible