Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
659
questions
3
votes
1
answer
96
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
52
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 ...
- 318
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
143
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
2
votes
1
answer
96
views
NP-hard $k$-SAT variant with exactly $\ell$ occurrences per variable
For the purpose of this post, let $k$-SAT be SAT with exactly $k$ literals per clause, as opposed to the more common meaning of at most $k$ literals per clause.
With the purpose of proving some ...
- 737
9
votes
2
answers
5k
views
Is SAT an existential question?
Some sources state that an algorithm that solves the SAT problem not only needs to decide whether a given existentially-quantified formula is satisfiable or not, but, additionally, in the case where ...
- 195
1
vote
1
answer
45
views
Possible to solve a combinatorial game with integer programming?
I recently had the idea that it would be neat if it were possible to make a SAT solver play combinatorial games. To start, I'm trying a relatively simple case of solving single-stack Misère Nim ...
- 290
1
vote
0
answers
108
views
CNF – satisfy at most a fixed number of clauses
I'm working on this task:
Prove that the following problem can be solved in time $2^{k} \cdot \Vert \varphi \Vert^{\mathcal{O}(1)}$: given a boolean formula $\Vert \varphi \Vert$ in CNF, decide ...
- 65
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 ...
- 11
0
votes
1
answer
77
views
Running time of SAT and other EXPTIME algorithms
I need to propose an algorithm for a NP-hard problem. I use dynamic programming which leads to a running time $O(2^s\cdot n^2), s\leq n.$ The algorithm aims to finding a path in a graph $G(V, E)$ (in ...
- 113
1
vote
1
answer
55
views
Is ANF-SAT P or NP?
Given a finite set of equations in ANF, for example:
$$
\begin{cases}
(x_1 \land x_2) \oplus (x_1 \land x_3 \land x_4) \oplus 1 = 0 \\
x_3 \oplus (x_2 \land x_3 \land x_4) = 0 \\
(x_1 \land x_4) \...
- 13
2
votes
1
answer
1k
views
Why can't 3-SAT be solved efficiently if you convert all clauses (x ∨ y ∨ z) into (u ∨ z) by introducing a variable?
Let $a_i$, $b_i$, etc., be a literal, i.e., a variable or the negation of a variable.
3-SAT concerns formulas in CNF form: $(a_1 \vee a_2 \vee a_3) \wedge \dots \wedge (b_1 \vee b_2 \vee b_3)$ (3-CNF)....
- 495
-1
votes
1
answer
166
views
How to prove that P = NP?
So if someone proves with an algorithm that SAT can be solved in deterministic polynomial time, then P = NP and that's it?
- 135
1
vote
1
answer
69
views
Simple Skolemization Question
Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
2
votes
0
answers
31
views
Reductions from 3-SAT that won't work directly from SAT
Our prof talked about why it's good to know that 3-SAT is NP-complete because it's easier to craft reductions from it than from plain SAT.
However, all the examples we've seen (reduction to ...
- 21
0
votes
0
answers
167
views
Polynomial Reduction from 3SAT
Given an undirected graph $G=(V,E)$ where $V$ is a set of vertices, and $E$ is a set of edges and
given a set $D$ where $D \subseteq V $ and $ \forall v \in V \setminus D \: \mid \: \exists w \in D : ...
- 1
0
votes
0
answers
52
views
Could we know what's the total number of unsatisfiable 3SAT formulas for a given n variables?
given some $n$ variables I would be interested to know what is the count of all 3SAT formulas under $n$ that are unsatisfiable.
An example of all 3SAT forumlas under $n=3$ is the following:
$$
( x \...
1
vote
1
answer
52
views
Reducing a mixed Boolean expression containing XOR of conjunctions
I know that XOR-SAT can be solved in polynomial time using arithmetic in $F_2$ and Gaussian elimination.
I have a set of formula that is of the form
$$
G_i := \oplus_{j=0}^{i} \left ( a_j \land b_{i-j}...
- 135
0
votes
0
answers
61
views
Can these variants of SAT/Tautology be actually pretty simple?
There are 8 (very similiar) languages I'd like to discuss here:
CNF SAT
DNF SAT
CNF No-SAT (Existence of a false assignment)
DNF No-SAT
CNF Tautology
DNF Tautology
CNF Contradiction
DNF Contradiction
...
-1
votes
1
answer
46
views
Can you help me find some examples of 3co-SAT for 4 variables?
I've been studying the examples of 3co-SAT recently.
It's easy to find an example of one variable.
$(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$
Examples of 2 ...
- 305
0
votes
0
answers
60
views
Why don't we consider that NP = co-NP while we can reduce Tautology problem into Satisfiability in polynomail time easily?
Let's determine if an expression is tautological or not and let's try this expression:
((a ⊼ b) ∨ c) ↔ (¬a ∨ ¬b ∨ c).
We can turn this problem into CIRCUIT-SAT decision problem by asking if the ...
- 45
0
votes
1
answer
36
views
CNF-SAT time complexity and input processing
Boolean Satisfiability (CNF-SAT) problem in $n$ variables may contain a CNF formula with $O(2^n)$ clauses in the worst case.
My question is: Wouldn't a program reading a CNF formula have to ...
- 135
1
vote
1
answer
93
views
MSAT and IMSAT problems (restricted versions of SAT)
I was reading about about NP-intermediate problems on Wikipedia and saw the IMSAT problem mentioned over there.
There is no Wikipedia page for that problem and they only cite this paper.
In the paper ...
- 113
1
vote
0
answers
41
views
Probability of a randomised algorithm solving SAT
Let WALKSAT be defined as follows:
Let $σ$ be a random truth assignment to the vars
For $t = 1, 2, . . . , 3n$:
◦ If $\phi$ is satisfied by $σ$, exit the loop
◦ Else, pick an unsatisfied clause $c$ ...
- 423
2
votes
1
answer
257
views
Complexity of the (Complete/Assign) 3-SAT problem?
A complete $k$-CNF formula on $n$ variables $(k\le n)$ is a $k$-CNF formula which contains all clauses of width $k$ or lower it implies.
Let us define the (Complete/Assign) 3-SAT problem: Given $F$, a ...
- 511
2
votes
2
answers
90
views
what does **input** mean for the $3SAT$ question? Is it the number of variables $n$ or the number of clauses $m$
We know that $3SAT \in NP$,
and the definition of $NP$ is as follows:
$NP$ is the class of languages that have polynomial time verifiers.
But I have a question:
what does input mean for the $3SAT$ ...
- 305
0
votes
1
answer
288
views
Time-complexity of evaluating a CNF formula
Given a Boolean formula over $n$ variables in CNF and a partial assignment to it, all the algorithms I can think of to evaluate the assignment run in time $\Theta(n^2)$. Is it possible to do it in $O(...
- 239
0
votes
0
answers
57
views
I need to show that the problem is NP-complete
Double-SAT = {𝜓: 𝜓 has at least two satisfying truth assignments}. Hint: reduce from SAT. Start with a formula 𝜑 and modify it to get a formula 𝜓 so that 𝜑 is satisfibale if and only if 𝜓 has at ...
- 11
0
votes
0
answers
126
views
Effecient encoding of sum equality in cnf+xor
I am wondering as to how to efficiently encode the following subcircuit for a binary satisfiability solver (cnf, and optionally xor clauses, if this helps):
...
- 1,404
0
votes
1
answer
32
views
reducing the word problem for dtm to sat / cnf-sat / 2-sat
word problem: given a language L through a deterministic turing machine, is the word w in the language L?
the problem should be decidable, since if there is a deterministic turing machine i can simply ...
- 11
3
votes
1
answer
101
views
Why can't $QBF$ be reduced to $SAT$
Let $QBF_k$ be the problem of determining the satisfiability of a formula of the form
$Φ = Q_1x_1Q_2x_2 . . . Q_kx_k φ(x_1, . . . , x_n)$.
where each $Q_i$
is one of the quantifiers $∀$ or $∃$. So, $Φ$...
- 423
2
votes
2
answers
155
views
Exponential Time Hypothesis and the input size vs number of variables
According to Exponential Time Hypothesis there does not exist a deterministic algorithm to solve SAT over $V$ variables in time $o(2^V)$. However, let's say the number of literals $n = \omega(poly(V))$...
- 1,429
1
vote
0
answers
157
views
Is there an alternative method to using Gaussian elimination in order to solve 3-XORSAT
I have a large system of $3$-$XORSAT$ constraints (i.e. up to $3$ variables per constraint) and this can be represented in matrix form as a linear algebra problem $Ax=b$ $mod$ $2$. Solvability (i.e. ...
- 11
1
vote
1
answer
83
views
Proving the NP hardness of two variants of SAT
$k$-$\text{RSAT}$ is a variant of $k$-$\text{SAT}$ where we restrict our attention to formulae in
which each variable occurs at most $3$ times, and each literal occurs at most twice. The language
$k$-$...
- 423
3
votes
1
answer
637
views
4-SAT but two literals per clause must be true
I'm trying to show that a modified 4-SAT in which at least two literals per clause must be true is NP-complete. I'll call it $4_2$-SAT. I understand the reduction from 3-SAT to 4-SAT, and I know why $...
- 31
1
vote
1
answer
62
views
Proving 2SAT is in P vs algorithm for finding a satisfying assignment
I want to understand the proof in the following link that 2SAT is in P. What is the need for the last corollary? Wouldn't be enough to just prove the case for the graph with the help of the path ...
- 113
4
votes
1
answer
466
views
What are efficient approaches to implement unit propagation in DPLL-based SAT solvers?
I'm trying to decompose deduction steps of DPLL algorithm -- unit propagation and pure literal elimination -- for parallelization. However, I want a baseline and asymptotic analysis to compare to my ...
- 43
3
votes
1
answer
114
views
Find the flaw in the 3SAT solver algorithm
I consider decision version of 3SAT problem.
Main idea is to find congruent clauses and construct such maximum formula,
which satisfiability/truth table won't be changed.
In case of unsatisfiable ...
4
votes
1
answer
482
views
3-SAT with atmost 3 variables and variable occuring once per clause
I've stumbled across this problem on CSES
https://cses.fi/345/task/E/
and was wondering is it somehow reducible to 2-SAT with given constraints?
So, the problem states that you need to solve a 3-SAT ...
2
votes
1
answer
60
views
expected running time of Randomwalk for k-SAT
model: gambler ruin theorem.
A gambler has $i$ coins initially, in every step, he wins a coin with probability $p$, and loses a coin with probability $1-p$. The expected time that he loses all his ...
- 318
0
votes
1
answer
84
views
Is there a version of the boolean satisfiability problem that has NC complexity?
Boolean satisfiability problem (SAT) is NP-complete by Cook–Levin theorem. (wiki)
Horn-satisfiability – given a set of Horn clauses, is there a variable assignment which satisfies them? This is P's ...
- 299
2
votes
1
answer
42
views
Satisfiability of bounded assignment of input variables to CNF formula
Consider a CNF formula $F$ such that all the literals in every clause must be negative ( here is an example : $F$ = ($\bar{x_{1}}$ $\wedge$ $\bar{x_{2}}$) $\vee$ ($\bar{x_{3}}$ $\wedge$ $\bar{x_{4}}$ $...
- 49
2
votes
0
answers
61
views
Quantum Boolean SAT algorithm?
Is there a quantum SAT algorithm, a quantum analogue of the DPLL or CDCL algorithms?
Note: I'm not looking for the quantum analogue of the Boolean satisfiability problem (though that would be ...
- 142
2
votes
1
answer
56
views
SAT and #SAT in Quantum
Let us look at the two questions that are NP-complete for a classical computer:
Given an arbitrary Boolean expression, find an assignment of variables that evaluates the expression to $0$ (SAT).
...
- 307
0
votes
2
answers
288
views
Integer/prime factorization to 3 SAT
So essentially as the title says, I just want to understand how its done. I have a light idea from my own research, but its failing at one point, and I feel it maybe due to crucial point missing in my ...
2
votes
1
answer
94
views
How to determine if clause will change the satisfiability of the 3SAT formula?
I have satisfiable 3SAT formula like:
(x1 or x2 or x3) and (not x1 or x2 or not x3)
and some clause which is not in this formula ...
1
vote
1
answer
31
views
Radius Local Search Algortihm for Max-Sat problem approximating ratio
Assume that in classical Local Search algorithm for MAX-SAT we could flip no more than $r
\leq n/2$ variables (let's call it $r$-flip) on every iteration. More precise: on every iteration we're ...
- 158
0
votes
1
answer
44
views
Can 3-SAT be recognized in less than exponential time?
Obviously it is an open question if $3$-SAT can be decided in a polynomial amount of time. But what results do we know about its recognizabilty? Can $3$-SAT be recognized in a polynomial amount of ...
- 147
1
vote
0
answers
47
views
Conflict Clusters – Another P=NP Proof [closed]
Conflict Clusters – Another P=NP Proof
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiability problem. Given an instance of clauses where each clause has three literals, is there a ...
- 341
2
votes
1
answer
231
views
Reducing a CNF formula to a DNF formula in less than exponential time
The easy way is by looking at the $\{0,1\}$-table and construct the corresponding DNF formula from that, but this will take $2^n$ time. I want to do it much more efficiently.
My idea is based upon the ...
- 334