# Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

618 questions
Filter by
Sorted by
Tagged with
1 vote
29 views

### Understanding the Strong Exponential Time Hypothesis

Let $n$ be the number of variables in the input formula and $m$ the number of clauses. Define $s_k = \inf\{\delta : k\text{-SAT can be solved in } 2^{\delta n} \text{ time}\}$. The strong exponential ...
• 15
28 views

### Problems with proof of NP-completness of SAT following Cooks original paper

I am currently in the process of trying to understand the original proof of NP-completeness of SAT given in the seminal paper by Cook [COOK71] and have struggled with a few of the details of the proof ...
44 views

• 219
30 views

### Correctness implication graph for 2-sat

i want to proof some stuff for the 2-sat problem. So we have something like this: $\varphi$ = (x$_{1}$ $\lor$ y$_{1}$) $\land$ (x$_{2}$ $\lor$ y$_{2}$) $\land$ ... $\land$ (x$_{n}$ $\lor$ y$_{n}$). We ...
• 11
46 views

### I need to show that the problem is NP-complete

Double-SAT = {𝜓: 𝜓 has at least two satisfying truth assignments}. Hint: reduce from SAT. Start with a formula 𝜑 and modify it to get a formula 𝜓 so that 𝜑 is satisfibale if and only if 𝜓 has at ...
• 11
54 views

### Effecient encoding of sum equality in cnf+xor

I am wondering as to how to efficiently encode the following subcircuit for a binary satisfiability solver (cnf, and optionally xor clauses, if this helps): ...
• 1,383
29 views

### reducing the word problem for dtm to sat / cnf-sat / 2-sat

word problem: given a language L through a deterministic turing machine, is the word w in the language L? the problem should be decidable, since if there is a deterministic turing machine i can simply ...
• 11
75 views

### Why can't $QBF$ be reduced to $SAT$

Let $QBF_k$ be the problem of determining the satisfiability of a formula of the form $Φ = Q_1x_1Q_2x_2 . . . Q_kx_k φ(x_1, . . . , x_n)$. where each $Q_i$ is one of the quantifiers $∀$ or $∃$. So, $Φ$...
• 391
119 views

### Exponential Time Hypothesis and the input size vs number of variables

According to Exponential Time Hypothesis there does not exist a deterministic algorithm to solve SAT over $V$ variables in time $o(2^V)$. However, let's say the number of literals $n = \omega(poly(V))$...
• 1,393
1 vote
100 views

### Is there an alternative method to using Gaussian elimination in order to solve 3-XORSAT

I have a large system of $3$-$XORSAT$ constraints (i.e. up to $3$ variables per constraint) and this can be represented in matrix form as a linear algebra problem $Ax=b$ $mod$ $2$. Solvability (i.e. ...
• 11
1 vote
65 views

1 vote
43 views

### Proving 2SAT is in P vs algorithm for finding a satisfying assignment

I want to understand the proof in the following link that 2SAT is in P. What is the need for the last corollary? Wouldn't be enough to just prove the case for the graph with the help of the path ...
• 113
21 views

### How overapproximation of boolean abstraction function works?

I just found that if original formula is unsat, using boolean abstraction function can result in sat. Clearly this is overapproximate. I wonder if I have contingent formula, does that means my boolean ...
179 views

### What are efficient approaches to implement unit propagation in DPLL-based SAT solvers?

I'm trying to decompose deduction steps of DPLL algorithm -- unit propagation and pure literal elimination -- for parallelization. However, I want a baseline and asymptotic analysis to compare to my ...
• 43