Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
657
questions
-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
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
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
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 ...
- 125
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
1
vote
1
answer
82
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
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
...
- 148
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 ...
- 148
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
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 ...
- 11
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
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(...
- 141
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 ...
- 1,429
-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 ...
- 1,429
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
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
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 ...
- 33
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 ...
- 1,151
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 ...
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
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
78
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 ...
- 103
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
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)
$$
...
- 13
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 ...
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
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 &...
- 213
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?
- 2,184
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
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 ...
- 213
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
0
votes
0
answers
48
views
Is this a valid method to merge clauses in CNF formulas?
Assume $$C_1 = (x_1 \lor x_2 \lor \lnot x_3)\hspace{0.2cm} C_2 = (x_4 \lor x_5 \lor x_3) \hspace{0.2cm} C_3 = (x_3 \lor x_5 \lor x_6)$$ Let
$$ \phi_1 = C_1 \land C_2 \land C_3$$ and
$$ \phi_2 = (x_1 \...
- 185
2
votes
0
answers
46
views
Modified DPLL for 3-SAT by reducing to 2-SAT
In Boolean Satisfiability of CNF formulae we have $k$-SAT where each clause has at most $k$ literals. It is well known that $k$-SAT is polynomial time reducible to $3$-SAT. It is also well known that $...
- 135
0
votes
1
answer
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 ...
- 318
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 $...
- 33
1
vote
1
answer
61
views
Is Horn-SAT with XOR-relations NP-complete?
I was wondering if the combination of Horn-SAT and XOR-SAT is solvable in polynomial time or not.
It seems they can be solved in polynomial time as both are in class P and also that Horn-SAT is P-...
- 33
1
vote
1
answer
19
views
Are the indices of variables in the formula variable?
Let $L$ be an arbitrary language in $\Sigma_3$. Thus it can be written that $x \in L \Leftrightarrow \exists y^{p(|x|)} \forall z^{p(|x|)} \exists w^{p(|x|)} \langle x,y,z,w \rangle \in B$ where $p(\...
- 2,932
1
vote
1
answer
50
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 ...
- 166
1
vote
0
answers
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....
- 133
1
vote
1
answer
66
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 ...
- 25
2
votes
0
answers
36
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 ...
- 121
0
votes
2
answers
53
views
Finding a 2SAT instance that has a specific solution set
Is there a 2SAT instance of variables $(a,b,c,d,e,f,g)$ that has exactly the solution set $S=\{ (1,0,0,0,0,0,0),(0,1,0,0,0,0,0),(0,0,1,0,0,0,0),(1,1,0,1,0,0,0),(1,0,1,0,1,0,0),(0,1,1,0,0,1,0),(1,1,1,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. ...
- 111
1
vote
1
answer
136
views
Variation of 3-SAT
I already know that SAT and 3-SAT are NP-complete.
If in 3-SAT the Boolean expression should be divided to clauses,such that every clause contains at most (in the original problem it says exactly) ...
- 47
1
vote
1
answer
101
views
How to reduce 3SAT to TwoOrMoreSAT?
I want to prove, that 2OrMoreSAT is NP-complete. It's defined as follows:
A formula is considered strongly satisfiable if there exists a model such that two or more different literals in every clause ...
- 11
0
votes
1
answer
85
views
MAX-SAT approximation factor
I am stuck on an exercise that ask the approximation factor of a MAX-SAT approximated algorithm generalized from a MAX-3SAT algorithm
MAX-3SAT:
set every variable with a random value ($0$ or $1$ each ...
- 3