# Questions tagged [satisfiability]

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

551 questions
Filter by
Sorted by
Tagged with
32 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? ...
15 views

### Check if the given satisfying assignment of CNF formula is lexicographically the first

If there is a CNF Boolean formula in $n$ variables then the potential satisfying assignments are the binary strings of length $n$. Given a CNF Boolean formula and a satisfying assignment how ...
49 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$?
168 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? ...
42 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 ...
418 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) ...
21 views

### Given a graph and specific VC instance, find number of variables when reducing from VC to SAT

I have question already answered from past exam, and I'm trying to figure where my logic fails. Given a graph find vertex cover of size 2. The question is how many variables are there going to be for ...
48 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 ...
63 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 ...
21 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 ...
33 views

32 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 ...
103 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 ...
27 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 ...
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 ...
88 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 ...
28 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 ...
38 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 ...
28 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 ...
32 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 ...
37 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 \...
30 views

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

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

### Multi-Objective Implicit Hitting Set for Multi-Objective MaxSAT

MaxSAT is a problem related to SAT where there is a finite collection of hard and soft clauses which share boolean variables. The hard clauses must be satisfied while the soft clauses have a weight. ...
61 views

### Complexity of All-SAT

All-SAT is the problem of enumerating all satisfying assignments of a boolean formula. All-SAT is different from #SAT, where it suffices to find the number of satisfying assignments without ...
28 views

### Looking for prior occurrences of $k$-CNF efficiently translated to coloring?

Has anyone else ever translated 3-cnf (4-cnf) on $N$ variables and $M$ clauses into 4 coloring on $O(M)$ vertices? By taking two variables from a clause, the four boolean combinations correspond to ...
36 views

### Is clause learning in SAT parsimonius?

I have a model counting program bob. On some graph coloring formulas, bob got the right answer only after removing clause learning. That is to say, with clause learning, bob sometimes counts ...
15 views

### What is the difference between NP and co-NP? [duplicate]

I'm trying to understand the very simple concept of co-NP but I can't figure it out. On wikipedia, it gives the example of SAT and its complement: The complement of any problem in NP is a problem in ...
86 views

### How is this reduction of 3-SAT to Half-SAT not valid? [duplicate]

I am studying algorithms and there is a question in CLRS called the Half-SAT problem We are given a 3-CNF formula with n variables and m clauses where m is even. We wish to determine whether there ...
65 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 ...
232 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 ...