Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
653
questions
0
votes
1
answer
34
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)$ ...
- 133
0
votes
0
answers
27
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
...
- 146
-1
votes
0
answers
9
views
Can SAT problems be divided into 2 classes: (1) those with reversible operations and (2) those with irreversible operations?
Can SAT problems be divided into 2 classes:
those with reversible operations
those with irreversible operations?
- 146
0
votes
2
answers
50
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 ...
- 146
0
votes
3
answers
78
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
62
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
12
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
11
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 ...
- 743
4
votes
2
answers
81
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
37
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,393
-1
votes
1
answer
35
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,393
1
vote
0
answers
23
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
66
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
483
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
58
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,106
0
votes
1
answer
39
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
29
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
57
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
58
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
40
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.♦
- 154k
1
vote
1
answer
60
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
31
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
55
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 ∨ ...
- 176
0
votes
1
answer
45
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 &...
- 203
0
votes
1
answer
37
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,240
0
votes
0
answers
28
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 ...
- 123
0
votes
1
answer
47
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 ...
- 203
4
votes
0
answers
37
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
11
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 ...
- 203
0
votes
0
answers
38
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
45
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
34
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 ...
- 176
0
votes
1
answer
31
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
54
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,933
1
vote
1
answer
48
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
47
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
57
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
50
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
70
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
76
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) ...
- 37
1
vote
1
answer
77
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
67
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
3
votes
1
answer
86
views
Finding a minimal set of package versions in a dependency graph with constraints
Suppose you have a dependency graph of "packages" registered in the ecosystem of a given programming language. We can model each package as a tuple ...
- 133
1
vote
1
answer
48
views
Question about a proof of the existence of unsatisfiable linear k-CNFs for any k
Today I am reading paper Unsatisfiable Linear k-CNFs Exist, for every k by Dominik Scheder, 2007. But I have some problem to understand the proof of Theorem $3.2$.
I don't know how to understand the ...
- 176
0
votes
1
answer
28
views
How to get the formal model using propositional logic
Input
There are three chairs (1,2,3) in the same row.
We need to find a seat for three guests (a,b,c).
Constraints
The first guest does not want to be seated next to the third one (neither left nor ...
0
votes
1
answer
120
views
Why solving #2SAT in polynomial time implies P = NP?
The wikipedia article for #P states that if we have a polynomial-time algorithm for a #P-complete problem, P = NP is true.
As #2SAT is #P-complete, this would mean that providing a polynomial-time ...
- 195