Questions tagged [3-sat]

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

Filter by
Sorted by
Tagged with
4
votes
1answer
116 views

Is there a 3-SAT problem 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? ...
1
vote
1answer
36 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?
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 ...
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 -- ...
0
votes
0answers
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 ...
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 ...
0
votes
2answers
29 views

Is the following problem NP-Complete? [closed]

3SAT with the additional condition that exactly 1 or 3 literals must evaluate to 1.
1
vote
1answer
63 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
16 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\...
2
votes
1answer
231 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
98 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 ...
0
votes
2answers
47 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 ...
5
votes
6answers
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?
0
votes
0answers
154 views

Reducing 3-SAT to restricted 3-SAT

I am trying to show that the following problem is NP-hard. Input: A boolean function in CNF (conjunctive normal form) such that every clause has at most three literals and every variable appears in at ...
1
vote
2answers
120 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
1answer
49 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 ...
1
vote
1answer
122 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 ...
0
votes
0answers
25 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
1answer
41 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 ...
3
votes
1answer
41 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 ...
0
votes
0answers
24 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?
1
vote
1answer
186 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....
2
votes
1answer
194 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
1answer
112 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 ...
1
vote
0answers
74 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{...
2
votes
2answers
519 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 ...
1
vote
1answer
38 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 ...
1
vote
1answer
208 views

How to prove finding two paths that are at least k edges apart is NP-hard?

Let $G=(V, E)$ be an unweighted, undirected, and connected graph. Given two start vertices $s_1$ and $s_2$ and two end vertices $t_1$ and $t_2$ is there a path from $s_1$ to $t_1$ and $s_2$ to $t_2$ ...
0
votes
0answers
57 views

How sub-exponential time does $\text{3SAT}$ have to be to make $\text{NP} \neq\text{EXP}$? What else would imply $\text{NP} \neq\text{EXP}$?

The exponential-time hypothesis posits that if $\mathsf{3SAT}$ has NO subexponential time algorithm (i.e. one in $\mathcal O(2^{o(n)})$), then $\mathsf{P}\neq \mathsf{NP}$. However, I am interested ...
1
vote
1answer
38 views

For given reduction f, can show "if f(x) in 4NAE then x in 3SAT", but not "if x is not in 3SAT then f(x) not in 4NAE"

Claim: $3SAT \le_p 4NAE $, where reduction $f$ is defined as such: given a 3CNF formula $\varphi$, add to each clause a new literal $z$ (where $z$ is same literal for each clause), and return new ...
10
votes
2answers
3k views

What is wrong with this simple proof of P=NP?

Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiabilty problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause ...
1
vote
1answer
224 views

Time complexities of state-of-the-art SAT solvers with respect to length of the formula

I am learning about DPLL and CDCL SAT solvers, and I know that they have time complexity exponential to the number of variables. If I am not mistaken, one of the reasons why most believe P does not ...
1
vote
1answer
158 views

Finishing degree requirements NP-complete: Choosing 1 element from each set avoiding conflicts

The question, which I have slightly paraphrased to get rid of the fat, is this: There are $k$ areas of study in which you need to take 1 course. For each area of study, there is a set of courses $C_1,...
3
votes
1answer
53 views

CNF satisfiability with a bound on number of clauses

Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
7
votes
1answer
708 views

Random restarts for unsatisfiable instances

In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice. ...
1
vote
2answers
140 views

Change the structure from 3SAT to 1in3 3SAT

There is a variable set V = {x1,x2,x3} and clause set C1={x1,x2,-x3} C2={x1,-x1,-x2} C3={-x1,-x2,x3} C4={x2,x3,-x3}. For this structure, no matter each variable is positive or negative, the clause can ...
1
vote
0answers
55 views

How does the number of clause affect the difficulty of a 3-SAT Problem? [closed]

It was asked here and closed although it is a very specific question witch was exactly answered in several papers. The complexity of 3-SAT problems has a phase transition which reaches the critical ...
0
votes
1answer
64 views

Descriptive complexity of 3SAT

lately I'm reading about descriptive complexity, which I find is a fascinating branch of computational complexity. I found many formulas in $\exists$$SO$ that describe problems with graphs but none ...
2
votes
1answer
80 views

3-CNF to "independent form"

Is it possible to convert all logical formulae into a form such that each variable ends up in exactly 1 "factor" of the and operation? ($\wedge$). Any combination of operations is allowed, though the ...
4
votes
0answers
100 views

What is the generating algorithm for the "komb" instances found on satcompetition.org?

For the 2017 and 2018 Random SAT Tracks of the SAT Competition ran by the International Conference on Theory and Applications of Satisfiability Testing there are small, yet difficult, random 3-SAT ...
2
votes
0answers
125 views

How many isomorphic 3SAT formulas?

For a 3SAT formula with $n$ variables and $m$ clauses, I am interested in counting the number of isomorphic formulas (isomorphic in the sense that they are logically equivalent and have the same ...
2
votes
1answer
75 views

3-SAT with negative-literals in each clause

Does a 3-SAT problem, where in each clause there is at least a negative-literal, always has a solution? After looking at it, seems to me that the answer is yes, but maybe there is something I am not ...
3
votes
0answers
48 views

Is a "stacked", "local" version of 3-SAT NP-hard?

In this previous question, I learned that if each variable in a string $C \in 3\text{-SAT}$ appears only "locally", then finding a satisfying assignment is no longer NP-hard. My question below builds ...
8
votes
1answer
538 views

Is a "local" version of 3-SAT NP-hard?

Below is my simplification of part of a larger research project on spatial Bayesian networks: Say a variable is "$k$-local" in a string $C \in 3\text{-CNF}$ if there are fewer than $k$ clauses ...
5
votes
1answer
197 views

Parametrized reduction from 3-SAT to Independent Set to lower bound running time under ETH assumption

I want to prove that, assuming Exponential Time Hypothesis is true, there is no algorithm that solves Independent Set in $2^{o(|V|+|E|)}$ time. I want to apply the following strong parameterized many-...
2
votes
2answers
625 views

Proof that POSITIVE-3-SAT is in the complexity class P

I have the following language: $$\text{POSITIVE-3-SAT} = \{\langle\phi\rangle \mid \phi\text{ is a satisfiable boolean formula in conjunctive normal form,}\\ \text{ in which all clauses consist of ...
0
votes
1answer
95 views

Resolution when clauses contain more than 1 complementary literals

Let's assume that we have clauses $(l_1 \lor l_2 \lor l_3), (\neg l_1 \lor \neg l_2 \lor l_4), (l_1 \lor l_2 \lor l_5), (\neg l_1 \lor \neg l_2 \lor l_6)$, where both $l_1$ and $l_2$ are complementary ...
1
vote
0answers
153 views

The NP completeness proof for a variation of the 3CNF-SAT problem

There is a variation of 3CNF-SAT which is called 10-3-CNF-SAT = {<$\Phi$>: $\Phi$ is a satisfiable CNF formula with $\textbf{at most}$ 3 literals per clause and every variable occurs in $\textbf{at ...
3
votes
2answers
188 views

Is every X3SAT instance with no cycles satisfiable?

Exactly 1 in 3 SAT (X3SAT) is a variation of the Boolean Satisfiability problem. Given a set of clauses, where each clause has three literals, is there an assignment such that in each clause exactly ...