Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more
6 votes
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 ...
orlp's user avatar
  • 13.6k
6 votes

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 ...
orlp's user avatar
  • 13.6k
4 votes

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 ...
Emil Jeřábek's user avatar
3 votes
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 ...
holf's user avatar
  • 946
3 votes
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 ...
D.W.'s user avatar
  • 160k
3 votes

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 ...
D.W.'s user avatar
  • 160k
2 votes

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-...
Bernardo Subercaseaux's user avatar
2 votes
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 ...
D.W.'s user avatar
  • 160k
2 votes
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,...
D.W.'s user avatar
  • 160k
2 votes

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 ...
Bernardo Subercaseaux's user avatar
2 votes
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 ...
Bader Abu Radi's user avatar
2 votes

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.
D.W.'s user avatar
  • 160k
2 votes
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 ...
D.W.'s user avatar
  • 160k
2 votes
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 ...
Emil Jeřábek's user avatar
2 votes
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 ...
Emil Jeřábek's user avatar
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 ...
D.W.'s user avatar
  • 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 ...
D.W.'s user avatar
  • 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 ...
orlp's user avatar
  • 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 ...
Kenneth Kho's user avatar
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 ...
Steven's user avatar
  • 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 ...
D.W.'s user avatar
  • 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 ...
Tim Vermeulen's user avatar
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 = ...
D.W.'s user avatar
  • 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, ...
D.W.'s user avatar
  • 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 ...
Jxb's user avatar
  • 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 $...
Jason Hu's user avatar
  • 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 ...
Benjamin Smus's user avatar

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