# Questions tagged [satisfiability]

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

588 questions
Filter by
Sorted by
Tagged with
19 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,272
25 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
16 views

### How can I create a reduction from a object state to a SAT problem? [closed]

I have a class with N boolean variables and M states. I wand to create an algorithm which is scaleable for N and M and allow me to check if a new rule in the state transition table can be satisfied. ...
• 101
42 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, $Φ$...
• 331
57 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,349
1 vote
28 views

### Sum in counting satisfying assignments

Is there a polynomial-time algorithm that computes the sum of two boolean formulas, such that, (#SUM(F,G) = #F + #G), the output satisfying assignments equals the sum of the satisfying assignments of ...
• 11
1 vote
52 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
42 views

1 vote
27 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
15 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 ...
68 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
66 views

### Find the flaw in the 3SAT solver algorithm

I consider decision version of 3SAT problem. Main idea is to find congruent clauses and construct such maximum formula, which satisfiability/truth table won't be changed. In case of unsatisfiable ...
68 views

### 3-SAT with atmost 3 variables and variable occuring once per clause

I've stumbled across this problem on CSES https://cses.fi/345/task/E/ and was wondering is it somehow reducible to 2-SAT with given constraints? So, the problem states that you need to solve a 3-SAT ...
44 views

### expected running time of Randomwalk for k-SAT

model: gambler ruin theorem. A gambler has $i$ coins initially, in every step, he wins a coin with probability $p$, and loses a coin with probability $1-p$. The expected time that he loses all his ...
• 113