# Questions tagged [satisfiability]

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

657 questions
Filter by
Sorted by
Tagged with
14 views

### Clique to SAT example explanation

We are at college trying to implement the reduction of the clique problem to a SAT problem but I dont quite get the examples of the slides if someone can give me a not so technical explanation of what'...
1 vote
57 views

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

I know that propositional satisfiability is NP-complete and that if I add first-order quantifiers I get the complete problems for the polynomial hierarchy and PSPACE. What happens if my formulas are ...
1 vote
48 views

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

I would guess that this question is going to make some people wonder how I haven't already found a solution looking through papers -- but I do not see a clear algorithm. In implementing CDCL, I read ...
17 views

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

I am going through Justin Thaler's book - https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf - "Proofs, Arguments, and Zero-Knowledge" He presents the Sumcheck protocol & then ...
27 views

### Number of clauses in SAT problems

I was going through the proof that DNF-SAT can be solved in polynomial time. The strategy was to go through all clauses, find a clause that doesn't contain both x and x' for any variable x and then ...
1 vote
84 views

### Specialized SAT solver (?)

(Context) Given two byte arrays of length 16, say $L$ and $H$, one can define a mapping $M$ from the set of all bytes to itself in the following way. If $0 \le b \lt 256$ is a byte, let $\text{lo}(b)$ ...
31 views

### Does the following down-voted answer not answer the question "Why does Schaefer's theorem not prove that P=NP?"?

Does the following highly down-voted answer not answer the question "Why does Schaefer's theorem not prove that P=NP?"? If not, why not? Marek, V. Wiktor. Introduction to Mathematics of ...
61 views

50 views

### Is it an open problem if CDCL algorithms violate SETH?

Strong Exponential Time Hypothesis states that general SAT, where clauses are not limited in length, can't be solved in time $o(2^n)$. It's proven that DPLL algorithm requires $\Omega(2^n)$ time in ...
36 views

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

Schaefer's dichotomy theorem ensures than when a constraint satisfiability problem satisfies certain conditions, the problem is either in $\mathsf P$ or is $\mathsf{NP}$-hard. Suppose the following ...
1 vote
30 views

### Shortest unsatisfiable 3-CNF that can't be refuted with narrow resolution?

Proof width (the size of the largest clause in a proof) plays an important part in refuting an unsatisfiable formula. If a formula has a bounded-width resolution proof of its unsatisfiability, then ...
67 views

### if it were shown that every algorithm that solves SAT must have complexity Ω(n^(log n)) then P≠NP?

Shouldn't this statement be false? To be true the implication should be P=NP or am I wrong? I can't find a formal proof
16 views

### Complexity Class of the Problem: Existence of Unsatisfying Interpretations in Boolean Formulas

What is the complexity class of the problem if there exist two different interpretations that do not satisfy a given Boolean formula? I believe the problem of existence of an interpretation that does ...
487 views

### Complexity of a variant of #Positive-2-SAT

#Positive-2SAT is the problem of counting the number of satisfying assignments to a given Positive 2-CNF formula i.e 2-CNF formulas in which each literal is a positive occurrence of a variable. The ...
1 vote
73 views

### Why is conjunctive normal form (CNF) "better" for SAT than disjunctive normal form (DNF)?

When hand-manipulating algebra DNF (sum of products) is easier than CNF (product of sums). Possibly because factoring is more difficult than expanding. So why is it the opposite for computational ...
43 views

### Should I remove equivalent variables in a CNF file to be used by a SAT solver?

My CNF file ends with many pairs of clauses that represent that two variables are equivalent (eg: -3 7, 3 -7, 5 -11, -5 11, etc.). Do most SAT solvers automatically pre-process these and replace every ...
43 views

### How to solve boolean SAT with equality constraints

Say I have boolean formula in form of a CNF(x1,x2,...) with $x_i$ being boolean variables. Testing the satisfiability of the CNF is the SAT problem, i.e. determine ...
67 views

### Finding a Polynomial Time algorithm for the 3-SAT Problem

Let us consider m clauses containing 3 variables each i.e. A1,A2,A3...Am . Let the total literals in consideration be n. Then each clause : Ai = (xr $\lor$ xs $\lor$ xt) where 1 $\le$ r,s,t $\le$n and ...
79 views

### SAT polynomial time

Hi I understood it is not currently possible to solve SAT in polynomial time. Does this mean we can not currently solve an expression with n different boolean variables or with m different symbols in ...
1 vote
95 views

37 views

### the size of nice tree decomposition

Recently, I am reading paper An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances, which use tree decomposition to give an upper bound for SAT resolution refutation. For a ...
38 views

1 vote
51 views

### Encoding "all-except" constraints in CNF

I am looking for an efficient CNF encoding of the following situation: I have sets of boolean literals $A = \{ a_1, \ldots, a_m \}$, $B = \{ b_1,\ldots, b_n \}$ and subsets $B_1, \ldots, B_m$, where ...
1 vote
54 views

### Restricted Planar 3-SAT NP-hard

As we all know, 3-SAT is NP-hard. Two of the less known results are that Planar 3-SAT is NP-hard and also a 'restricted' 3-SAT, where any literal appears in at most two clauses turns out to be NP-hard....
1 vote
67 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 ...