# Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

659 questions
Filter by
Sorted by
Tagged with
69 views

### Stalmarck's method: x ≡ x → z, does z have to be true?

I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that: y $\to$ z $\equiv$ x where x, y and z are booleans which ...
83 views

### Attempt to reduce to problem of inner product

The problem of Orthogonality: gives $n$ vectors of dimension $k$ and another set of same, can a pair be found with inner product = $0$? The problem of max product: likewise two sets each $n$ vectors (...
270 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 vote
43 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-...
35 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 ...
966 views

### Prove TILING is NP-Complete

I have a homework task to show that $\mathrm{TILING} = \{(T, 1^N) \mid \text{it is possible to cover } N \times N \text{ square with tiles from }T\}$, where $t\in T$ is $C^4$ for some color set $C$, ...
76 views

### Resolution algorithm does not seem to generate the empty clause

Let's assume I have the following 3 clauses: $\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$ and I want to see if our KB entails $\neg U$ so I tried to apply ...
146 views

### Is 2-SAT over Linear Real Arithmetic in P or NP?

The general boolean satisfiability problem (SAT) is NP-complete, and thus can't be solved in polynomial time (assuming $P \neq NP$). But the special case of 2-SAT is in P, and can be solved in linear ...
59 views

### Why proofs of Cook's Theorem assume k is given (n^k for NTM)?

A typical proof of Cook-Levin's Theorem proceeds like this: Suppose problem X is in NP. Then there is an NTM M deciding X in time n^k, for some k. Given a word w, NTM M, and k, we construct a Boolean ...
796 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 ...
65 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 ...
68 views

### Algorithm to reduce a Circuit-SAT to NAND-SAT

I am trying to construct an algorithm to reduce OR, AND and NOT gates into NAND-SAT. Can someone give me a hint as to where to start?
1 vote
141 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 ...
381 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? ...
64 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$?
356 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? ...
77 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 ...
1k 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) ...
123 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 ...
313 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
22 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 ...
536 views

47 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 ...
375 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
35 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 ...
132 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
98 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 ...
420 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 ...
311 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
52 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 ...
57 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 ...
97 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 \...
42 views

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

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