Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
659
questions
1
vote
2
answers
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 ...
- 2,184
3
votes
4
answers
2k
views
Why isn't SAT in coNP?
I understand why NP=coNP if SAT is in coNP (How do I prove that SAT in coNP implies NP=coNP?).
But I'm missing why the following machine doesn't turing recognize the complementary of SAT:
Given a ...
-1
votes
0
answers
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
0
answers
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 ...
- 33
0
votes
1
answer
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 ...
CommunityBot
- 1
1
vote
1
answer
141
views
Best compression algorithm for CNF SAT instances in DIMACS
For a CNF SAT instance in the DIMACS format what is the best algorithm to compress it? What is the best algorithm for 3-SAT instances in particular?
In 2020 SAT competition used .xz which if I ...
CommunityBot
- 1
15
votes
3
answers
9k
views
Prove NP-completeness of deciding satisfiability of monotone boolean formula
I am trying to solve this problem and I am really struggling.
A monotone boolean formula is a formula in propositional logic where all the literals are positive. For example,
$\qquad (x_1 \lor x_2) ...
1
vote
1
answer
93
views
Boolean constraints for a connected component of a graph
Suppose I have an undirected graph $G=(V,E)$, and boolean variables $x_v$ (one for each vertex $v \in V$). These variables select a subset $S \subseteq V$ of vertices, namely the vertices $S=\{v \mid ...
D.W.♦
- 156k
5
votes
3
answers
1k
views
Are there any open source SAT solvers with UNSAT core extraction algorithm built in?
Just like the title says. I need to use a SAT solver on a series of CNF formulas but not only do I need an answer of the type satisfiable/unsatisfiable but also some subset of clauses whose ...
- 1
0
votes
1
answer
37
views
Complexity of this variant of the Monotone(+,2−) -SAT problem?
In this post,Monotone$(+, 2^-)$-SAT problem is defined as follows:
Given a monotone CNF formula $F^+$, where each variable appears exactly once (as a positive literal), and a monotone 2-CNF formula $...
CommunityBot
- 1
3
votes
1
answer
511
views
How to encode reachability in a graph with walls as a SAT problem
Suppose we have a graph that represents a grid of cells. We are given a cell to start in and a cell that's the destination. There are cells that we cannot enter and they are known as walls. Finally we ...
CommunityBot
- 1
0
votes
1
answer
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 ...
D.W.♦
- 156k
2
votes
2
answers
2k
views
Simplest transformation from XOR to CNF SAT
What is the simplest way to transfrom $a\newcommand*\xor{\oplus}b=c$ to a CNF SAT expression with minimum number of clauses. The default transformation requires upto 9 clauses. I think we can do much ...
- 318
0
votes
0
answers
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
2
votes
1
answer
97
views
Proving satisfiability using resolution and variable elimination
I don't 100% understand this. But I have a entailment, and I want to prove whether it is satisfiable or not, and I will do this using resolution and variable elimination.
Here is the formula:
$$
(x_1 \...
CommunityBot
- 1
2
votes
2
answers
3k
views
Unique SAT complexity clarification
Unique SAT is defined as:
Given any SAT problem, does the SAT problem have exactly 1 solution?
As I understand it is co-NPHard. I am unclear how it is in co-NP
Assuming the problem has more than 1 ...
- 1,429
1
vote
1
answer
65
views
Logical Consequence - Equivalent Assertions
I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
CommunityBot
- 1
1
vote
1
answer
80
views
Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?
I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ...
CommunityBot
- 1
1
vote
1
answer
83
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)$ ...
D.W.♦
- 156k
0
votes
0
answers
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
...
- 142
1
vote
1
answer
66
views
A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?
I am working on an LRA Theory solver for SymPy, an open source python library for symbolic computations. You can find my work here. Currently I'm trying to optimize it to run faster.
My implementation ...
CommunityBot
- 1
1
vote
1
answer
43
views
Can you transform 3sat (or equivalent) into another satisfiability problem that increases the ratio of solutions to non-solutions
Say I have f(x1,x2,x3,...) where the output is either 0 for all inputs (unsatisfiable) or a variable boolean output of 0 or 1 depending on the input (satisfiable). Let's not consider functions that ...
CommunityBot
- 1
12
votes
3
answers
2k
views
Why does Schaefer's theorem not prove that P=NP?
This is probably a stupid question, but I just don't understand. In another question they came up with Schaefer's dichotomy theorem. To me it looks like it proves that every CSP problem is either in P ...
- 142
0
votes
2
answers
59
views
Can any SAT problem be converted to a system of linear equations over $\mathbf{Z}_2$?
Can any SAT problem be converted into one with only affine formulas?
Handbook of Satisfiability p. 672:
Affine formulas. A linear equation over the two-element field is an expression of the form $x_1 ...
- 142
0
votes
3
answers
82
views
Is there a 2SAT encoding for a NAND gate
I am trying to encode some circuit checking algorithms, but encountered difficulty creating a 2SAT representation for a NAND circuit. Is there a proof that this is not possible?
- 1,188
0
votes
0
answers
13
views
Reference request for Unit Clause Based SAT Reduction Rules
I tested my XSAT solver using the 4 pigeons in 3 holes problem converted to XSAT. The pigeon hole instance I give below had 108 variables and 88 clauses after being converted to monotone XSAT. My ...
- 341
0
votes
1
answer
43
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 ...
CommunityBot
- 1
0
votes
0
answers
16
views
Reduction of $3SAT$ to $2P2N-3SAT$ (without trivial clauses)
Given an instance of $3SAT$ the objective is to reduce it directly to $2P2N-3SAT$ without the reduction having any 'trivial' clauses. The trivial clauses can be where the same variable in a clause is ...
- 753
4
votes
2
answers
87
views
Finding a vector of maximum Hamming distance from a subspace of $(\mathbb{Z}/2\mathbb{Z})^n$
Let $W$ be a linear subspace of the vector space $V = (\mathbb{Z}/2\mathbb{Z})^n$. Let $k = \dim(W)$. For $v \in V$, define the distance from $v$ to $W$ to be $d(v,W):=\min_{w\in W} d(v,w)$ where $d(...
- 570
0
votes
3
answers
893
views
Reducing Graph Reachability to SAT (CNF)
So I came across this problem in my textbook. I was wondering how to develop a reduction from the Graph Reachability problem to SAT (CNF) problem. (i.e. formula is satisfiable iff there exists a path ...
CommunityBot
- 1
-1
votes
1
answer
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 ...
D.W.♦
- 156k
1
vote
0
answers
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 ...
- 25
0
votes
0
answers
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
1
vote
1
answer
72
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 ...
CommunityBot
- 1
0
votes
0
answers
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 ...
- 1
10
votes
2
answers
3k
views
What is wrong with this simple proof of P=NP?
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiabilty problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
- 143
0
votes
0
answers
56
views
Why weakening rule doesn't increase the size of resolution refutation?
I am studying the complexity of SAT resolution refutation. There is a useful tool named weakening rule
The weakening rule:
B -->B ∨ C
says that from a clause B we can derive the weaker clause B ∨ ...
- 318
0
votes
1
answer
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 ...
- 21.6k
0
votes
1
answer
40
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 ...
- 161
1
vote
1
answer
62
views
Encoding SAT EqualsK Constraint with Two Possible Values
I am wondering about a way to CNF encode an EqualsK constraint with two possible values. In other words, I want to solve for the equation:
$$
(\sum_{i=1}^n x_i = A) \lor (\sum_{i=1}^n x_i = B)
$$
...
D.W.♦
- 156k
0
votes
0
answers
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 ...
-1
votes
1
answer
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 ...
- 267
0
votes
1
answer
44
views
What's the relation between DPLL and BDDs?
BDDs are a way of representing Boolean formulas.
DPLL is an algorithm to determine satisfiability of Boolean formulas.
My understanding is that the two are used for SAT solving.
How are they combined?
CommunityBot
- 1
0
votes
1
answer
55
views
SAT with every variable occuring exactly once
With the Circuit-SAT problem, I often see the "split" gate (I don't know the official name of it). This gate has a truth table of:
$$
\begin{array}{|c |c c|}
0 & 0 & 0\\
1 & 1 &...
- 1,720
0
votes
0
answers
41
views
If $\overline{3SAT}\in BP\cdot NP$ then $PH=\Sigma_3^P$
I have the problem
If $\overline{3SAT}\in BP\cdot NP$ then $PH=\Sigma_3^P$
To solve this I am using a result $BP\cdot NP\subset NP/poly$ which I can prove (not doing here). I have two solutions but ...
- 133
2
votes
2
answers
362
views
Circuit satisfiability problem : SAT-C to SAT-2C
I have the following language : $L=\{\langle C_1,C_2\rangle \text{ | } C_1 \text{ and } C_2 \text{ are two circuits that calculate different function}\}$. We can call this language SAT-2C.
Prove that ...
CommunityBot
- 1
0
votes
1
answer
68
views
Time complexity to convert a truth table to a boolean circuit
The SAT problem is often explained in terms of truth tables. Given some random boolean circuit, calculate its truth table; does there exist an output of $1$ in the truth table?
But how about going the ...
CommunityBot
- 1
4
votes
0
answers
45
views
Benchmark of SAT solvers on random k-SAT instances at satisfiability threshold
I am looking for a solid reference (peer-reviewed publication) on the design and/or benchmarking of SAT solvers for random k-SAT ($4 \leq k \leq 8$) operating at satisfiability threshold.
The majority ...
- 41
0
votes
0
answers
10
views
Do you resolve all clauses in the processed bucket in the Davis-Putnam algorithm?
I'm reading the description and example of Davis-Putnam on page 102 of the Handbook of Satisfiability and I'm confused by the example they use.
To start with, they fill the following buckets
$C: \{\...
- 101
0
votes
0
answers
12
views
Would proving that finding a satisfiable input is intractable prove that SAT is intractable? [duplicate]
With the SAT problem, there is a corresponding search variant. Given an arbitrary boolean expression, find a given input such that the output of the boolean expression is $1$. To my knowledge, this ...
- 213