New answers tagged

1

To show that Vertex Cover and 3SAT is "equivalent", you have to show that there is a 3SAT satisfaction if and only if there is a k vertex cover in the graph constructed in the reduction step. Assuming you are familiar with how the reduction is done, (if not ,refer to the document). Since you only asked about how this setup proves that if there exists a k-...


5

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around. SAT and SMT solvers ...


1

Does this always work on larger matrices with 2*n rows and 2*n+1 columns where n is the number of variables? (I think it may need non-redundant (linearly independent?) rows.) It works but since there are assignments other than -1 and 1, how will you use the row echelon form to make any conclusions about the 1-in-3 SAT instance? Two cases: Case 1: The 1-...


5

Let me recap the proof. We are given a sparse NP-hard language $A$: for each length $n$, there are at most $n^c$ strings of length $n$ in $A$. For a satisfiable CNF $\varphi$, let $a(\varphi)$ be the lexicographically first satisfying assignment for $\varphi$. We consider the NP language $B$, which consists of all pairs $(\varphi,w)$ such that $\varphi$ is ...


2

This problem is NP-hard (and in addition hard to approximate and W[1]-hard), because maximum independent set can be reduced to it. Reduction: Each variable represents a vertex and each clause represents an edge.


3

The result you are trying to prove is known as Mahaney's theorem. It is covered by textbooks on complexity theory, and in many online lecture notes. The proof in Jonathan Katz' lecture notes indeed uses LEXSAT.


2

If you want to know whether there exists a general method/algorithm which can convert any given mathematical statement (by which you mean statements written in logic (say first-order logic, second-order logic ... etc)) to a SAT formula which is True iff that statement is True, then the answer is No. The reason being that evaluating whether an SAT formula ...


1

It depends on the mathematical statement. If it has the form $$\exists x_1 \in S_1 \cdots \exists x_n \in S_n . \varphi(x_1,\dots,x_n)$$ where $\varphi(x_1,\dots,x_n)$ is some condition on $x_1,\dots,x_n$ and $S_1,\dots,S_n$ are finite sets, then yes, it can be expressed as a 3CNF formula in a straightforward way. However, statements like $\exists x \in ...


0

Here is something your oracle can do: if you are given two formulas $\alpha,\beta$, and are guaranteed that at least one of them is satisfiable, then you can find one of them which is satisfiable by calling $M(\alpha,\beta)$: if $M(\alpha,\beta) = 1$ then $\alpha$ is satisfiable, and if $M(\alpha,\beta) = 0$ then $\beta$ is satisfiable. Given a satisfiable ...


1

Problem A is reducible to Problem B in following manner: Pick a variable in problem A and set it to 0 Now we have a formula of size n-1, if satisfiable with B then return satisfiable Else, pick problem A again and set the variable to 1 Now we have a formula of size n-1 again, if satisfiable with B then return satisfiable else return unsatisfiable In ...


1

Any algorithm that decides the satisfiability of a formula can also be used to find an assignment for a satisfiable formula: While not all variables are assigned: Pick a variable and choose value 0. If formula is no longer satisfiable, replace value with 1.


3

Such a reduction is described in Appendix B of Régis Barbanchon, On unique graph 3-colorability and parsimonious reductions in the plane. Barbanchon attributes it to previous work ([9] in the bibliography). Elsewhere, I have seen an attribution to Schaefer's celebrated paper in which he proves his famous dichotomy theorem, among else giving a reduction from ...


4

Yes, a 3-SAT formula $\phi$ can be transformed into a 1-in-3 SAT formula $\phi'$ while preserving the number of satisfying assignments. To avoid ambiguities I will use "$\vee$" between literals of a 3-SAT clause, and commas between literals of a 1-in-3 SAT clause. Let me preliminarily show that, given two literals $a$ and $b$, we can simulate a new type of ...


2

Consider the following CNF: $$ (a \lor \lnot b) \land (\lnot a \lor b) \land (a \lor b). $$ It has a unique satisfying assignment, $a=b=\top$, which satisfies the last clause twice. However, if you remove the last clause, then you get another satisfying assignment, $a=b=\bot$.


Top 50 recent answers are included