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
69
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
83
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 (...
- 125
2
votes
1
answer
270
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 ...
- 435
1
vote
1
answer
43
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
35
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 ...
- 494
6
votes
1
answer
966
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
76
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 ...
- 143
3
votes
1
answer
146
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
59
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,055
3
votes
3
answers
796
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 ...
- 125
0
votes
3
answers
65
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 ...
- 305
0
votes
1
answer
68
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
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 ...
- 11
3
votes
1
answer
381
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
-1
votes
1
answer
64
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
356
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
77
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
1k
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
1
answer
123
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 ...
- 305
5
votes
1
answer
313
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 ...
- 837
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 ...
- 326
2
votes
1
answer
536
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\...
1
vote
1
answer
433
views
Reduction of K-Vertex-Cover to SAT: How to define the constraint?
Overall, one would naturally think that with n different nodes, and for x(1) for example representing node 1, it would be like:
x(1)+x(2)+x(3)...+x(n) <= k
This would mean that for every possible ...
1
vote
1
answer
684
views
How to convert Bipartite Perfect Matching to SAT?
SAT is $NP$-complete while Bipartite Perfect Matching is in NC under derandomization assumptions. How to convert Bipartite Perfect Matching from balanced bipartites to SAT without Cook-Levin?
- 2,881
2
votes
0
answers
41
views
Under ETH: $\exists$ Problem unsolvable in $2^{o(n)}$ $\Leftrightarrow^?$ 3-SAT can be represented in linear bits
It is a popular open question if there is a problem unsolvable in $2^{o(n)}$ on inputs with $n$ bits, assuming ETH. I recommend reading that question first. That question states that, assuming the ETH ...
- 2,469
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 ...
- 753
4
votes
1
answer
719
views
Is 3-UNSAT problem coNP-complete?
The 3-SAT problem, i.e. the problem whether a given Boolean formula consisting of clauses of at most 3 literals is known to be NP-complete. Then it’s complement, i.e. whether such a formula is ...
- 145
1
vote
1
answer
96
views
Three dimensional matching expressed as SAT
The posting in the website Embedding SATISFIABILITY into 3-DIMENSIONAL MATCHING seeks $3SAT$ as a $3$ dimensional matching instance.
I am looking to solve the converse problem. How to solve three ...
- 2,881
1
vote
2
answers
231
views
Converting non-deterministic TM to deterministic TM using poly time SAT solver
Suppose there exist deterministic turing machine $M$ that could solve SAT in polynomial time. How can we construct a deterministic TM $N$ ,by using SAT solver $M$, that take as input a non-...
user139795
2
votes
0
answers
48
views
Necessary condition for 3-CNF unique satisfiability
I need to iterate through all formulas of 7 variables in 3-CNF which have unique satisfying assignment (1,1,1,1,1,1,1).
I could iterate through all formulas which are true under that assignment -- ...
- 121
4
votes
2
answers
72
views
Compact representation for quantified boolean formula
I got black-box (too big to analyze) boolean formula f(...) with 3 sets of input arguments: $x_1... x_i, y_1... y_j, z_1... z_k$. And I want to find such values for x-arguments that for every y-...
- 113
3
votes
1
answer
490
views
Reduction from the SAT problem to the NAE-SAT problem
I study complexity and computation independently.
I have a problem that I can not solve.
That's the problem:
For the SAT problem, there is a version in which we receive as input phrase $\varphi$ in ...
- 123
1
vote
0
answers
80
views
How to design an unbounded Monte Carlo algorithm for SAT(Boolean Satisfiability Problem) problem?
I want the algorithm to be in polynomial time and the correct answer rate is 0.5 or more. (True / false judgment is polynomial time)
All the methods I think of take exponential time(2^n).
Can anyone ...
- 23
1
vote
1
answer
123
views
SAT formula for connected graphs on the grid
In the answer to an earlier question "SAT algorithm for determining if a graph is disjoint" a formula is constructed that is satisfiable iff a given graph is connected.
The formula uses a ...
- 29.8k
2
votes
1
answer
65
views
Number of queries for $NP^{NP}$
So a few days ago my lecturer told us that for every nondeterministic polynomial time oracle
machine $M$, there is a nondeterministic polynomial time oracle machine $N$ that gives us $L(N^{3-SAT}) = L(...
- 121
4
votes
1
answer
47
views
Is there a $L$-complete variant of SAT?
Many complete problem of different class of complexity has SAT variant. Like 3-SAT or $k$-SAT is $NP$-complete, Horn-SAT is $P$-complete, 2-SAT is $NL$-complete, and so on. So I was wondering if there ...
- 43
3
votes
1
answer
375
views
Why is it useful to transform 0-1 integer programming problem into SAT problem?
There are several researches studying translating 0-1 integer programming into CNF form. For example, this paper and this C++ library. As the lecture notes here goes, translating 0-1 integer ...
- 33
1
vote
1
answer
35
views
Computational complexity of dividing a set of constraints into a minimum number of satisfiable clusters
I am looking for the computational complexity of the following problem.
Divide a given set of constraints into a minimum number of satisfiable clusters such that the constraints within the same ...
- 21
0
votes
0
answers
132
views
Prove that following 3-CNF is SAT
Let $\phi$ be a 3-CNF expression with the properties
Every variable can be used at most 3 times
No Variable can be used twice in a term
Show that you can always choose the truth-value of the ...
- 157
1
vote
1
answer
98
views
Incomplete definition of function- first order logic
Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations.
Let $\Sigma_2=\{c',g^2,R_1'^1,...,R_k'^1\}$ where $c'$ is constant, $g$ is ...
- 99
2
votes
1
answer
420
views
NP-Hardness of Half-SAT (at least half clauses)
I'm solving Problem 14.14 of What can be computed?.
14.14 Consider the computational problem HALFSAT defined as follows. The
input is a Boolean formula B in CNF. If it is impossible to satisfy at ...
- 27
-1
votes
1
answer
311
views
NP Reduction - Dominating set to SAT
Given a graph G and an integer k , recognize whether G contains dominating set X with no more than k vertices. And that is by finding a propositional formula ϕG,k that is only satisfiable if and only ...
- 1
1
vote
1
answer
52
views
Is there CIRCUIT-SAT algorithms that slightly depends on gates count?
For 3CNF-SAT problems exists a lot of algorithms that still have exponential complexity, but work faster than brute force. The complexity of this algorithm based on a number of variables or the number ...
- 113
0
votes
1
answer
57
views
NP-completeness of variant SAT: SAT-5Clauses
I'm solving Problem 14.4 of What can be computed?.
14.4 Define the decision problem SAT-5CLAUSES as follows. The input is a Boolean formula B in CNF. The solution is “yes” if it is possible to ...
- 27
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 \...
- 21
0
votes
2
answers
42
views
Is the following problem NP-Complete? [closed]
3SAT with the additional condition that exactly 1 or 3 literals must evaluate to 1.
- 31
3
votes
1
answer
62
views
Has it been shown or can we show that if $SAT \in P$ then SAT can't be in any complexity class C so that $C \subsetneq P$?
I'm already guessing that the answer is no because we cannot know whether there is a class "in between" already known classes? Or can we?
I am very new to complexity theory.
Thanks for any ...
user136613
2
votes
1
answer
55
views
How to represent bottom element (integer domains) in SMT formula
I'm doing some work with static analysis and need to represent local variables as SMT formulas. In general this is fairly straight forward, depending on the domain of the static analysis. However, ...
- 23
2
votes
1
answer
195
views
Complexity of All-SAT
All-SAT is the problem of enumerating all satisfying assignments of a boolean formula.
All-SAT is different from #SAT, where it suffices to find the number of satisfying assignments without ...
- 194
-1
votes
1
answer
52
views
Is clause learning in SAT parsimonius?
I have a model counting program bob. On some graph coloring formulas, bob got the right answer only after removing clause learning. That is to say, with clause learning, bob sometimes counts ...
