Questions tagged [3-sat]

3SAT is a famous special case of the boolean satisfiability problem (SAT).

Filter by
Sorted by
Tagged with
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 ...
user avatar
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 ...
user avatar
  • 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 $...
user avatar
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 ...
user avatar
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 ...
user avatar
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) \...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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-...
user avatar
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 ...
user avatar
-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 ...
user avatar
  • 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? ...
user avatar
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?
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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? ...
user avatar
  • 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$?
user avatar
  • 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? ...
user avatar
  • 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 ...
user avatar
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?
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 -- ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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.
user avatar
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 ...
user avatar
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\...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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?
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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?
user avatar
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....
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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{...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 683