Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
551
questions
1
vote
0answers
32 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?
...
0
votes
0answers
15 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 ...
-1
votes
1answer
49 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$?
5
votes
1answer
168 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?
...
0
votes
1answer
42 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 ...
2
votes
3answers
418 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) ...
0
votes
0answers
21 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 ...
0
votes
1answer
48 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 ...
2
votes
1answer
63 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 ...
1
vote
0answers
21 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 ...
1
vote
1answer
33 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
1answer
61 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
1answer
37 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
votes
0answers
31 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
votes
1answer
35 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 ...
3
votes
1answer
81 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 ...
1
vote
1answer
20 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 ...
1
vote
2answers
105 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-...
2
votes
0answers
22 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 -- ...
3
votes
2answers
51 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-...
5
votes
1answer
94 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 ...
1
vote
0answers
53 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 ...
1
vote
1answer
29 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 ...
2
votes
1answer
48 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(...
3
votes
1answer
32 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 ...
2
votes
1answer
103 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 ...
1
vote
1answer
27 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 ...
0
votes
0answers
52 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 ...
1
vote
1answer
88 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 ...
2
votes
1answer
28 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 ...
0
votes
1answer
38 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
vote
1answer
28 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 ...
0
votes
1answer
32 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 ...
2
votes
1answer
37 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 \...
0
votes
2answers
30 views
Is the following problem NP-Complete? [closed]
3SAT with the additional condition that exactly 1 or 3 literals must evaluate to 1.
3
votes
1answer
34 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 ...
2
votes
1answer
39 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, ...
0
votes
0answers
17 views
Multi-Objective Implicit Hitting Set for Multi-Objective MaxSAT
MaxSAT is a problem related to SAT where there is a finite collection of hard and soft clauses which share boolean variables. The hard clauses must be satisfied while the soft clauses have a weight. ...
1
vote
1answer
61 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 ...
0
votes
0answers
28 views
Looking for prior occurrences of $k$-CNF efficiently translated to coloring?
Has anyone else ever translated 3-cnf (4-cnf) on $N$ variables and $M$ clauses
into 4 coloring on $O(M)$ vertices? By taking two variables from a clause,
the four boolean combinations correspond to ...
0
votes
1answer
36 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 ...
1
vote
0answers
15 views
What is the difference between NP and co-NP? [duplicate]
I'm trying to understand the very simple concept of co-NP but I can't figure it out. On wikipedia, it gives the example of SAT and its complement:
The complement of any problem in NP is a problem in ...
2
votes
1answer
86 views
How is this reduction of 3-SAT to Half-SAT not valid? [duplicate]
I am studying algorithms and there is a question in CLRS called the Half-SAT problem
We are given a 3-CNF formula with n variables and m clauses where m is even. We wish to determine whether there ...
1
vote
1answer
65 views
Minimal unsatisfiable core algorithm
Wikipedia says that
There are several practical methods of computing minimal unsatisfiable cores.
but I cannot find any. I suppose that “practical methods” means polynomial algorithms. Be careful, a ...
2
votes
1answer
232 views
NOT satisfiable 3SAT instance certificate
Given a NOT satisfiable 3SAT instance, that we say $S$. Suppose that $M$ is a minimal subset of clauses of $S$ such that $M$ is NOT satisfiable. Say $X$ the subset of variables of $S$ that belong to ...
1
vote
0answers
99 views
Which features can be considered for neural network based SAT solving?
I'm trying to implement SAT solver, based on backtracking algorithm and BCP. This SAT solver is trying to pick one literal from each clause, from 3-CNF SAT instances. I've implemented a neural network ...
1
vote
1answer
56 views
Not satisfiable 3SAT instance implications
Suppose we have an instance of 3SAT that is NOT satisfiable and we say $S$.
If in $S$ there are the following $8$ clauses
$\left(a\vee b\vee c\right)\wedge\left(a\vee\bar{b}\vee c\right)\wedge\left(a\...
0
votes
0answers
49 views
Can anyone explain the pigeon-hole encoding method in proportional logic
Someone there who worked with cardinal contraindications within the framework of propositional logic? I have a problem understanding the pigeon-hole method. It is a method of satisfaction. I have been ...
0
votes
0answers
59 views
IF satisfiability problem belonged to P, can the certificate be found efficiently?
IF SAT(satisfiability problem) belongs to P, then is it possible for a certificate of an arbitrary instance of SAT to be found efficiently?
1
vote
0answers
104 views
Reduction between Parity-SAT and approximate counting
Consider two problems as defined here.
Approximate counting: Given a Boolean function $f(x)$, for $x \in \{0, 1\}^{n}$, distinguish between the two cases:
The number of satisfying assignments for $f(...
