# Questions tagged [3-sat]

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

132 questions
Filter by
Sorted by
Tagged with
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? ...
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?
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 ...
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 ...
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 -- ...
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 ...
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 ...
29 views

### Is the following problem NP-Complete? [closed]

3SAT with the additional condition that exactly 1 or 3 literals must evaluate to 1.
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 ...
16 views

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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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-...
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 ...
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 ...
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 ...