# Tag Info

Accepted

### SAT formulation of the condition that an even number of a given set of variables must be set to true

Let $\oplus$ be XOR, then your question is asking for $\bigoplus_{k=1}^n x_k = 0$. We can encode this efficiently without an exponential explosion in clauses by introducing new variables. The basic ...
• 13.6k

### P=NP? A reduction of CNF boolean satisfiability to the circulation problem in an undirected graph

Consider the CNF formula $a \wedge \neg a$. This has two clauses, $a$, and $\neg a$. If I understand your scheme correctly this maps to the following flow problem: This clearly has a solution (1 flow ...
• 13.6k

### Tseitin formula on 2-connected graph

Clearly, whether a formula is minimally unsatisfiable depends on the exact details of how it is formulated, so let me give a specific definition of Tseitin formulas. Given a graph $G=(V,E)$ and a ...
• 1,232
Accepted

### SAT solvers for counting the number of solutions

Yes, they are known as #SAT solvers. Some of them are exact, some of them are approximate. Some of them are based on a version of DPLL that exhaustively find every solution in a factorized way. Some ...
• 946
Accepted

### How fast can we make generalized k-SAT?

Worst-case bounds on running time are usually not very informative for SAT solvers. In particular, on problem instances that arise in practice, often SAT solvers run a lot faster than the bounds ...
• 160k

### Can any SAT problem be converted to a system of linear equations over $\mathbf{Z}_2$?

Equivalence: Not every SAT instance can be expressed as a system of linear equations. For instance, $x_1 \lor x_2$ cannot be expressed as a system of linear equations. (Why not? Systems of linear ...
• 160k

### Finding a vector of maximum Hamming distance from a subspace of $(\mathbb{Z}/2\mathbb{Z})^n$

Your problem is very likely NP-hard. If you don't add the restriction that $W$ is sub-space, but just receive a set of boolean vectors $W$, then it is NP-hard and known as a Covering Radius proven NP-...
Accepted

### How does the sumcheck protocol help solving the #SAT (circuit satisfiability) problem?

It doesn't solve SAT in faster than exponential time. It solves #SAT (not SAT), and the prover still needs exponential time. It doesn't give you the values which satisfy the circuit. It doesn't need ...
• 160k
Accepted

### Specialized SAT solver (?)

The best solution I know of is to use a SAT solver. I don't know whether there is a better solution. I don't see any proof that an arbitrary 3SAT problem can be reduced to it. (OK, strictly speaking,...
• 160k

### Is there a 2SAT encoding for a NAND gate

It seems, based on the comments in other answers, that what you are after is a 2-CNF formula $\phi(q, a, b)$ equivalent to $q \iff \overline{a \land b}$. This is indeed not possible; the only possible ...
Accepted

### Reduce CNF-SAT to decision problem

It is not clear in your solution why treating clauses as groups helps. Note that a satisfying assignment should induce a set of groups and vice versa. Hint: a non direct reduction (but you can start ...
• 2,921

### How to find a satisfying assignment in polynomial time without the use of randomness?

As mentioned by Clement C. on CS Theory, this is answered at Conditions for tractability of 3SAT-Satisfiability. You can even replace 1% with any other positive constant.
• 160k
Accepted

### Is boolean formula equivalence problem for 2-CNFs $\mathsf{coNP}$-hard?

I believe the problem is in $P$. Let $\varphi,\psi$ be the two 2-CNF formulas. The plan of approach will be to test satisfiability of $\varphi \land \neg \psi$ and of $\psi \land \neg \varphi$. If ...
• 160k
Accepted

### Resolution on weakening rule by derived clause

What proof of the completeness of resolution do you know? Chances are it can be easily adapted to this more general setting. Alternatively, you can reduce it to plain completeness. One way is as ...
• 1,232
Accepted

### Is there a linear programming method that is polynomial in the number of variables, constraints and bitlength of numbers?

Interior-point methods such as Khachiyan’s and Karmarkar’s are, indeed, polynomial in the size of the input, i.e., in the number of variables, constraints, and the bitlength of the coeficients. This ...
• 1,232
1 vote
Accepted

### Size of circuit generating the solutions of a SAT problem

Here is a plausibility argument that $C$ will need to be large in at least some cases. Let $H$ be a cryptographic hash function (model it as a random oracle). Define $H(x)[i]$ to be the $i$th bit of ...
• 160k
1 vote

### how to polynomially check if a given boolean formula is unsatisfiable

We don't know for sure, but most people expect the answer is "no". In particular, assuming NP != co-NP (as is a commonly held conjecture), the answer is "no". Checking that a ...
• 160k
1 vote
Accepted

### how to polynomially check if a given boolean formula is unsatisfiable

NP only requires you to have a polynomial size proof for "yes" instances. co-NP is the class of problems that requires polynomial size proofs for "no" instances. SAT is in NP, but ...
• 13.6k
1 vote
Accepted

### How to find a satisfying assignment in polynomial time without the use of randomness?

For refresher, let's first remember (Wikipedia) that we can convert any Boolean expression into conjunctive normal form, which is defined as conjunction ("AND" $\land$) of one or more ...
• 656
1 vote
Accepted

### Is it possible to find reductions from problems in $\mathsf{NP}$ to SAT based solely on the certificate verification algorithm?

Finding a reduction to SAT is easy but tedious. Write down a description of polynomial-time Turing machine $T$ that checks the certificate (as you have argued in your question, such a Turing machine ...
• 29.5k
1 vote

### Complexity of satisfiability for relational logic on the booleans

Nothing much changes. Every relation $R(x_1,\dots,x_n)$ is equivalent to $\exists t_1,\dots,t_m . \varphi(x_1,\dots,x_n,t_1,\dots,t_m)$ for some fresh variables $t_1,\dots,t_m$ (see the Tseitin ...
• 160k
1 vote

### How to find the learned clause from a UIP cut

First, some observations: Setting all literals in a reason set to true leads to a conflict through unit propagation. One can replace a non-decision literal from a reason set with its in-neighbors in ...
1 vote

### Is there a 2SAT encoding for a NAND gate

There is no proof that it is impossible, but it is believed that it's unlikely to be possible, because if you could convert every circuit with NAND gates to 2CNF, you would have a proof that P = ...
• 160k
1 vote
Accepted

### Schaefer's dichotomy theorem and limits on the formula length

Schaefer's theorem is stated in many places, e.g., on Wikipedia. Can you define a set $S$ of relations so that your problem has the form specified in Schaefer's theorem? No, you cannot. Therefore, ...
• 160k
1 vote

### Simplest transformation from XOR to CNF SAT

I'd like to offer a more straightforward method for transforming XOR equations into SAT. step 1: Regardless of the number of variables on the right side of the equality, we can shift them to the left ...
• 318
1 vote

### Reducing Graph Reachability to SAT (CNF)

Since the other two answerers really didn't put thought into this question, I think I should give a genuine encoding for subsequent readers. We consider a 2D matrix $R(i, j)$ meaning that the vertex \$...
• 632
1 vote

### Prove NP-completeness of deciding satisfiability of monotone boolean formula

IMO, it is intuitive to reduce Vertex-Cover to the problem that you are describing (which will show that the problem you are describing is at least as hard as Vertex-Cover). At the core of the problem ...

Only top scored, non community-wiki answers of a minimum length are eligible