# Questions tagged [satisfiability]

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

684 questions
Filter by
Sorted by
Tagged with
1 vote
37 views

### Applications of a SAT Solver Oracle for Determining the Uniqueness of Solutions

I am exploring two kinds of model $π_{π,π,k}$ and $S_{m,n,k}$ within the realm of satisfiability problems (SAT). Formal construction of $π_{π,π,k}$ To construct the $π_{π,π,k}$ model in ...
• 338
83 views

14 views

### Finding a common variable value among all SAT solutions

Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
1 vote
13 views

### Are there ASICs optimized to solve the SAT problem?

Are there ASICs (application-specific integrated circuits) optimized to solve the SAT problem, such as by the DPLL algorithm?
• 154
10 views

### Check if sum of positive integers is less than a W integer in CNF

As title says, what I am trying to do is to find a way to sum integers and later compare them with another integer W, in a manner that when the sum of integers is less or equal than W, using only CNF. ...
70 views

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

The picture below shows how to reduce the Boolean Satisfiability problem in CNF to the circulation problem in undirected graph (see here). As you can see, a[i] are ...
35 views

• 498
194 views

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

Lets say I have a SAT problem with variables $x_1,...,x_n$. For a given subset of the variables I want to create a clause which forces an even number of the variables in $S$ to be true. Of course ...
• 225
873 views

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

Assume that we are given a formula in 3-CNF such that at least 1% of the complete assignments satisfy it. My question is how to find a satisfying assignment in polynomial time without the use of ...
• 327
1 vote
44 views

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

The following problem has made me ask this question: Given a boolean formula $\varphi(X)$ decide if there exists a quantification of $\varphi(X)$ with $k$ $\forall$ quantifiers that holds true. ...
• 1,674
1 vote
23 views

### CNF Horn-renamability to 3-CNF Horn-renamability reduction?

A CNF formula is Horn-renamable if you can invert variables in such a way that each clause has at most one positive literal. There is an algorithm based on a reduction to 2-SAT given in Renaming a Set ...
• 1,674
1 vote
116 views

### Reduce CNF-SAT to decision problem

Given CNF-SAT reduce it to the following decision problem: Given n items, m groups (and for each group a set of items) and a ...
• 183
17 views

### Does $\mathsf{NC_1\subsetneq NC}$ imply $\mathsf{NP\neq coNP}$?

Any $\mathsf{NC}$ circuit could be presented in SAT form via Tseytin transform. This applies in the reverse too: an arbitrary SAT instance could encode any $\mathsf{NC}$ circuit. Now, Frege proof ...
• 1,674
79 views

### The parameterized complexity of Weighted-CNF-SAT parameterized by the number of clauses

What is the parameterized complexity of Weighted-CNF-SAT, when parameterized by the number of clauses? Input: A CNF formula $\phi$ with $m$ clauses and $n$ variables, and an integer $k$. Parameter: $m$...
28 views

### Is it possible to perform clause-pair minimization on a CNF instance in $o(n^2)$ time?

Let $\varphi(X)$ be a boolean formula in CNF over a set $X$ of boolean variables $x_1,x_2,...,x_n$. Let $c_i$ denote $i^{th}$ clause in $\varphi(X)$. $x_j^0$ denotes $\overline{x_j}$ and $x_j^1$ ...
• 1,674
1 vote
24 views

### Are there any SAT outside of $\mathsf{RP}$ variants that are solvable in quasipolynomial time?

It's possible to construct SAT problems that are solvable in quasipolynomial time, but they are also solvable in polylogarithmic space. Consider, for example, the following problem: Let a set $S$ ...
• 1,674
1 vote
22 views

### SAT for clauses of the form "At most m out of n are false"

Recall some terminology: Let $\mathsf P$ be a finite set of propositional atoms, and let $\Phi$ be a proposition over $P$ that is generated from $\top$, $\bot$, $\neg$, $\wedge$, and $\vee$. Then: A ...
• 111
25 views

### Computational Learning Problem: 3-DNF Reduction

I'm not sure how to solve this problem. Problem statement is: Consider the binary classification problem where X = R d and Y = {0, 1}. Consider the class of Binary classifiers given by intersection of ...
1 vote
59 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 ...
• 2,194
1 vote
162 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 ...
22 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 ...
• 125
34 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
104 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)$ ...
• 145
33 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 ...
• 154
81 views

• 141
87 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 ...
• 1,674
45 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,674
1 vote
44 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 ...
• 25
68 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
17 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 ...
501 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 ...
• 43
1 vote
188 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 ...
48 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 ...
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 ...