Questions tagged [3-sat]
3SAT is a famous special case of the boolean satisfiability problem (SAT).
154
questions
1
vote
1
answer
150
views
Proof that 2-sat is P-hard?
i figured out this is what i want to know:
in Cook's theorem it is shown that SAT is NP-hard. he shows it by showing that sat is at least as difficult like the word problem for nondet. Polynomial Time ...
- 11
2
votes
1
answer
34
views
Complexity of a restricted SAT problem
I am wondering about the complexity of the following SAT related problem:
Given a CNF with $n$ clauses containing exactly $k$ literals with the following properties:
The intersection of any pair of ...
- 23
3
votes
1
answer
94
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
3
votes
1
answer
67
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
69
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 ...
1
vote
1
answer
55
views
CNF clause to 3-SAT
How to transform a k-SAT CNF clause into a combination of 2-SAT and/or 3-SAT (1-SAT) clauses? $k>3$
Example 5-SAT:
$$ Q = \neg A \lor B \lor C \lor D \lor E $$
$$ \; \; = (X0 \lor X2 \lor X3) \...
0
votes
2
answers
58
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
0
votes
1
answer
43
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
1
answer
123
views
How to reduce 3-SAT to Set Splitting
I've been reading through Garey & Johnson's "Computers and intractability", and a problem SP4 caught my attention. It is stated as following:
Given a collection $C$ of subsets of a ...
- 13
2
votes
1
answer
48
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
2
votes
1
answer
64
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 ...
-1
votes
1
answer
43
views
Prove that T3SAT is NP-Complete
Instance: A boolean formula f(x1, . . . , xn) in 3CNF form, with m clauses labelled C1, . . . , Cm.
Is there an assignment to x1, . . . , xn such that every third clause is False and all other clauses ...
- 11
2
votes
2
answers
65
views
3SAT: Get smallest number of algorithm invocations to get a satisfiable assignment? How should it be done?
My Question is, what is meant with smallest number N. Does it mean I should try every possible constellation of the n variables and put each one of them into the formula φ and then use 3Sat on that? ...
- 73
0
votes
0
answers
31
views
Parameterized complexity of 3-SAT
Is the 3-SAT problem with $s$ variables and $t$ clauses FPT, parameterized by $s+t$,
or W[1]-hard, or para-NP-hard?
- 53
2
votes
3
answers
169
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
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
-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
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
1
answer
110
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,822
4
votes
1
answer
180
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
32
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,822
2
votes
0
answers
29
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
0
votes
0
answers
30
views
Show that $3SAT$ is a polynomial reduction on $MSAT$, i.e. $3SAT \leq_p MSAT$ [duplicate]
The exact definition of $3SAT$ and $MSAT$ are as follows:
$3SAT :=$ each clause has exactly 3 literals
$MSAT :=$ At least half of the literals of every clause are True
My intuition was, as we know ...
- 59
0
votes
0
answers
58
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 ...
- 147
0
votes
2
answers
39
views
Is the following problem NP-Complete? [closed]
3SAT with the additional condition that exactly 1 or 3 literals must evaluate to 1.
- 31
1
vote
1
answer
87
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
1
answer
21
views
Padding a 2SAT clause
In http://web.mit.edu/neboat/www/6.046-fa09/rec8.pdf, I see that they pad a 2SAT clause $(x\vee y)$ to make it a 3SAT clause by writing $(x\vee y\vee p) \wedge (x\vee y\vee \neg p)$. Why doesn't $(x\...
- 23
2
votes
1
answer
278
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
0
answers
121
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 ...
- 71
0
votes
2
answers
52
views
Oracle that can only definitively say if an instance is unsatisfiable
Assuming I have an Oracle that takes as input a strictly 3SAT Boolean instance and states whether the instance is satisfiable or not. If it says instance is unsatisfiable then the instance is ...
- 25
5
votes
6
answers
2k
views
Can anyone give me an instance of 3SAT with exactly one solution?
I need an instance of 3SAT with exactly one solution but I cannot think of or find one anywhere. Can anyone please give me an example?
- 77
1
vote
2
answers
210
views
Is there any algorithm for 3SAT problem that is fast and relatively easy to implement?
Here is the description for 3SAT satisfiability problem. I already know about the DPLL algorithm, but it's implementation is pretty complex. I would like some algorithm that is relatively simpler but ...
1
vote
1
answer
57
views
1-OR-3-SAT is in P
1-OR-3-SAT:
Input: 3-CNF formula $\varphi$
Question: whether there is an assignment $x$ such that in each clause there are one or three true literals.
I need to show that this problem is in $P$. I ...
- 158
1
vote
1
answer
293
views
Showing resolution algorithm for 2SAT is polynomial time
I don't quite understand why the resolution algorithm completes in polynomial time for 2SAT but not 3SAT.
I'm looking at slide 42 of these slides for reference. It is clear that given two clauses of ...
- 13
0
votes
0
answers
29
views
3-OCC-MAX SAT np-complete?
Assuming 3-OCC-MAX SAT is the language of all CNF formulas in which every variable appears in at most 3 clauses. Is this problem NP-Complete? I'm trying to find a karp reduction between SAT and this ...
2
votes
1
answer
49
views
algorithm for checking satisfiability
In order to prove that SAT is in NP, I need to come up with a polynomial time verfier (an algorithm). The Cooks Levin Theorem uses a non-deterministic Turing machine but that's not what I am looking ...
- 123
3
votes
1
answer
43
views
Is MAX-averageSAT a well-known problem?
Is there any variant of the Boolean SAT or Max-SAT problem that has a flavor of maximizing or minimizing the average of the weights of the satisfied clauses of a WCNF formula? Any literature on an ...
- 31
0
votes
0
answers
26
views
planar 1-in-3 sat described as a planar graph for independent set
Given a planar 1-in-3 sat formula, can someone reduce that formula into a graph that asks the question when ever there is an independent set for it, that's also planar?
- 21
1
vote
1
answer
302
views
Is Monotone 3-SAT with exactly 3 distinct variables untractable?
I have given the following SAT variation:
Given a formula F in CNF where each clause C has exactly 3 distinct literals and for each C in F either all literals are positive or all literals are negated....
- 155
2
votes
1
answer
209
views
Proof for NP-hardness of simultaneous minimization and maximization of a weighted subset
I am working on a problem defined as the following
Given a set of $n$ elements called $R \subseteq \mathbb{N} \times \mathbb{N}$ and numbers $Z,G \in \mathbb{N}$, where $Z$ is a measure of our ...
0
votes
1
answer
151
views
When does Gaussian elimination solve exact 1-in-3 SAT?
Terms:
A literal is a variable or its negation.
A clause is a set of literals.
An exact 3-in-1 clause is satisfied if an assignment of values to variables results in exactly 1 ...
- 351
1
vote
0
answers
94
views
CircuitSAT to 1-in-3SAT
This question follows
Unique 3SAT to Unique 1-in-3SAT
Consider an AND gate such that (A ∧ B) = C. It can be trivially expressed in 3SAT with 4 clauses and no extra variables.
$$
(A ∨ B ∨ \overline{...
- 683
2
votes
2
answers
801
views
Unique 3SAT to Unique 1-in-3SAT
Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment.
It was made from a binary multiplication circuit where I multiplied two primes numbers A and B such ...
- 683
1
vote
1
answer
83
views
Unique 1-in-3 SAT
Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment.
I know the value of each bit of the unique assignment because it was made from a binary ...
- 683