Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
588
questions
0
votes
0
answers
19
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,272
0
votes
1
answer
25
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
0
votes
0
answers
16
views
How can I create a reduction from a object state to a SAT problem? [closed]
I have a class with N boolean variables and M states.
I wand to create an algorithm which is scaleable for N and M and allow me to check if a new rule in the state transition table can be satisfied.
...
- 101
3
votes
1
answer
42
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, $Φ$...
- 331
2
votes
1
answer
57
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,349
1
vote
1
answer
28
views
Sum in counting satisfying assignments
Is there a polynomial-time algorithm that computes the sum of two boolean formulas, such that, (#SUM(F,G) = #F + #G), the output satisfying assignments equals the sum of the satisfying assignments of ...
- 11
1
vote
0
answers
52
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
42
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$-$...
- 331
3
votes
1
answer
93
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
27
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
0
votes
0
answers
15
views
How overapproximation of boolean abstraction function works?
I just found that if original formula is unsat, using boolean abstraction function can result in sat. Clearly this is overapproximate. I wonder if I have contingent formula, does that means my boolean ...
4
votes
1
answer
68
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
66
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 ...
- 199
4
votes
1
answer
68
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
44
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 ...
- 113
0
votes
1
answer
51
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 ...
- 287
2
votes
1
answer
25
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
28
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 ...
- 145
2
votes
1
answer
33
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).
...
- 297
0
votes
2
answers
56
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
33
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 ...
- 199
1
vote
1
answer
29
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
0
answers
34
views
Polynomial reduction to SAT with a condition
Let L be in NP.
Is there always a reduction from L to SAT where atleast m-1 clauses (m being the number of clauses in the CNF formula) can be satisfied?
When w is in L it is trivial because the ...
0
votes
1
answer
42
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
31
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
46
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 ...
- 314
3
votes
1
answer
42
views
Stalmarck's method: x ≡ x → z, does z have to be true?
I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that:
y $\to$ z $\equiv$ x
where x, y and z are booleans which ...
- 53
4
votes
1
answer
73
views
Attempt to reduce to problem of inner product
The problem of Orthogonality: gives $n$ vectors of dimension $k$ and another set of same, can a pair be found with inner product = $0$?
The problem of max product: likewise two sets each $n$ vectors (...
2
votes
1
answer
63
views
What is the maximal length of a CNF formula?
The question is quite short. Let $k$ be a given number. What is the maximal length of $k$-CNF formulae can we compute, over the set of binary variables $\left\{ x_1 ,\ldots, x_n \right\}$?
The way I ...
- 1
1
vote
1
answer
32
views
Trying to understand 3-SAT self-subsuming process
Trying to understand 3-SAT self-subsuming process
I've been studying solver theory and am trying to understand some of the basic concepts that I've been reading. In particular, the idea of self-...
- 21
2
votes
0
answers
33
views
Non-trivial reduction form SAT to $3$-SAT
Looking for any idea for reduction from $SAT \leq 3-SAT$ where $SAT$ is known to have $d$ variables at most in each clause. I am looking for a reduction in which the resulting formula will not depend ...
6
votes
1
answer
421
views
Prove TILING is NP-Complete
I have a homework task to show that $\mathrm{TILING} = \{(T, 1^N) \mid \text{it is possible to cover } N \times N \text{ square with tiles from }T\}$, where $t\in T$ is $C^4$ for some color set $C$, ...
- 63
2
votes
1
answer
41
views
Resolution algorithm does not seem to generate the empty clause
Let's assume I have the following 3 clauses:
$\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$
and I want to see if our KB entails $\neg U$ so I tried to apply ...
- 43
3
votes
1
answer
97
views
Is 2-SAT over Linear Real Arithmetic in P or NP?
The general boolean satisfiability problem (SAT) is NP-complete, and thus can't be solved in polynomial time (assuming $P \neq NP$). But the special case of 2-SAT is in P, and can be solved in linear ...
- 133
2
votes
1
answer
32
views
Why proofs of Cook's Theorem assume k is given (n^k for NTM)?
A typical proof of Cook-Levin's Theorem proceeds like this:
Suppose problem X is in NP. Then there is an NTM M
deciding X in time n^k, for some k. Given a word w,
NTM M, and k, we construct a Boolean ...
- 1,016
2
votes
3
answers
168
views
Why can $2$-SAT be solvable efficiently, but $3$-SAT not?
I am aware that 2SAT is polynomial while 3SAT is not, but I am looking for an intuition why its so. After all, even in 2SAT we can attempt all possible truth functions and its $2^n$. So I am hoping ...
0
votes
3
answers
44
views
For 3CNF unsatisfiable boolean formulas, does it take exponential time to transform them into disjunctive form？
From the link Solving SAT by converting to disjunctive normal form, I learnt that the algorithm to transform any boolean formula to disjunctive form takes exponential time in worst case.
But I have a ...
- 141
0
votes
1
answer
39
views
Algorithm to reduce a Circuit-SAT to NAND-SAT
I am trying to construct an algorithm to reduce OR, AND and NOT gates into NAND-SAT. Can someone give me a hint as to where to start?
1
vote
1
answer
82
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 ...
- 11
3
votes
1
answer
145
views
Smallest 3-SAT problem that no one has been able to solve?
In number theory progress is sometimes guided by people stating a specific Diophantine equation that they don't know how to solve.
Is there anything similar in the field of Boolean satisfiability?
...
- 31
0
votes
0
answers
42
views
Check if the given satisfying assignment of CNF formula is lexicographically the first
If there is a CNF Boolean formula in $n$ variables then the potential satisfying assignments are the binary strings of length $n$. Given a CNF Boolean formula and a satisfying assignment how ...
- 31
-1
votes
1
answer
60
views
Quasilinear time algorithm for 3-SAT
Is it consistent with the current knowledge that there is an algorithm solving a 3-SAT instance in $n$ clauses in quasilinear time in $n$?
- 31
5
votes
1
answer
225
views
Is there an instance of 3-SAT in less than 100 variables that no one has been able to solve?
In number theory, progress is sometimes guided by people stating a specific Diophantine equation that they don't know how to solve. Is there anything similar in the field of Boolean satisfiability?
...
- 51
0
votes
1
answer
43
views
Boolean formula for graph 3COL
For a given undirected graph $G=(V,E)$ I'm trying to construct a boolean polynomially computable formula $\varphi$ with the following property: $\varphi$ is satisfiable $\iff$ vertices of $G$ can be ...
- 115
2
votes
3
answers
522
views
Why is SAT based on the CNF?
I have been reading up on Boolean logic and, specifically, the Boolean satisfiability problem. I have seen several people mention that the expression must be converted to conjunctive normal form (CNF) ...
- 133
0
votes
0
answers
28
views
Given a graph and specific VC instance, find number of variables when reducing from VC to SAT
I have question already answered from past exam, and I'm trying to figure where my logic fails.
Given a graph find vertex cover of size 2.
The question is how many variables are there going to be for ...
- 219
0
votes
1
answer
65
views
For Turing machines, if the input variables increase, will the state set Q increase ? will the tape alphabet Γ increase?
For Turing machines, if the input variables increase, will the state set Q increase ? will the tape alphabet Γ increase?
For example, for the SAT problem, the first question is whether the Boolean ...
- 141
3
votes
1
answer
97
views
How hard is random SAT?
There is plenty of research into the so-called "random SAT" problem, where we basically try to solve SAT instances with clauses chosen "at random" in some sense.
There are all ...
- 690
1
vote
0
answers
22
views
Software/library to generate Ising models for random $k$-sat problems
Could someone point me to a software/library which lets one to generate the Ising model/spin model for random $k$-sat problems or $k$-sat problem of a given structure?
I understand that it will be ...
- 294
2
votes
1
answer
91
views
Reduction from SAT to SAT with exactly k true variables
Let $L$ be defined as follows:
$\small L = \{(\phi, k) \mid \phi \in SAT \mbox{ and there is a satisfying assignment for $\phi$ having exactly $k$ true variables} \}$
I am struggling to show that $SAT\...
