Questions tagged [satisfiability]

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

Filter by
Sorted by
Tagged with
1
vote
0answers
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? ...
0
votes
0answers
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 ...
-1
votes
1answer
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$?
5
votes
1answer
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? ...
0
votes
1answer
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 ...
2
votes
3answers
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) ...
0
votes
0answers
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 ...
0
votes
1answer
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 ...
2
votes
1answer
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 ...
1
vote
0answers
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 ...
1
vote
1answer
33 views

Reduction from SAT to SAT with exactly k true variables

Let $L$ be defined as follows: $\small L = \{(\phi, k) \mid \phi \in SAT \mbox{ and there is a satisfying assignment for $\phi$ having exactly $k$ true variables} \}$ I am struggling to show that $SAT\...
1
vote
1answer
61 views

Reduction of K-Vertex-Cover to SAT: How to define the constraint?

Overall, one would naturally think that with n different nodes, and for x(1) for example representing node 1, it would be like: x(1)+x(2)+x(3)...+x(n) <= k This would mean that for every possible ...
1
vote
1answer
37 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?
2
votes
0answers
31 views

Under ETH: $\exists$ Problem unsolvable in $2^{o(n)}$ $\Leftrightarrow^?$ 3-SAT can be represented in linear bits

It is a popular open question if there is a problem unsolvable in $2^{o(n)}$ on inputs with $n$ bits, assuming ETH. I recommend reading that question first. That question states that, assuming the ETH ...
2
votes
1answer
35 views

Simplest transformation from XOR to CNF SAT

What is the simplest way to transfrom $a\newcommand*\xor{\oplus}b=c$ to a CNF SAT expression with minimum number of clauses. The default transformation requires upto 9 clauses. I think we can do much ...
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 ...
1
vote
2answers
105 views

Converting non-deterministic TM to deterministic TM using poly time SAT solver

Suppose there exist deterministic turing machine $M$ that could solve SAT in polynomial time. How can we construct a deterministic TM $N$ ,by using SAT solver $M$, that take as input a non-...
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 -- ...
3
votes
2answers
51 views

Compact representation for quantified boolean formula

I got black-box (too big to analyze) boolean formula f(...) with 3 sets of input arguments: $x_1... x_i, y_1... y_j, z_1... z_k$. And I want to find such values for x-arguments that for every y-...
5
votes
1answer
94 views

Reduction from the SAT problem to the NAE-SAT problem

I study complexity and computation independently. I have a problem that I can not solve. That's the problem: For the SAT problem, there is a version in which we receive as input phrase $\varphi$ in ...
1
vote
0answers
53 views

How to design an unbounded Monte Carlo algorithm for SAT(Boolean Satisfiability Problem) problem?

I want the algorithm to be in polynomial time and the correct answer rate is 0.5 or more. (True / false judgment is polynomial time) All the methods I think of take exponential time(2^n). Can anyone ...
1
vote
1answer
29 views

SAT formula for connected graphs on the grid

In the answer to an earlier question "SAT algorithm for determining if a graph is disjoint" a formula is constructed that is satisfiable iff a given graph is connected. The formula uses a ...
2
votes
1answer
48 views

Number of queries for $NP^{NP}$

So a few days ago my lecturer told us that for every nondeterministic polynomial time oracle machine $M$, there is a nondeterministic polynomial time oracle machine $N$ that gives us $L(N^{3-SAT}) = L(...
3
votes
1answer
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 ...
2
votes
1answer
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 ...
1
vote
1answer
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 ...
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 ...
1
vote
1answer
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 ...
2
votes
1answer
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 ...
0
votes
1answer
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 ...
1
vote
1answer
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 ...
0
votes
1answer
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 ...
2
votes
1answer
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 \...
0
votes
2answers
30 views

Is the following problem NP-Complete? [closed]

3SAT with the additional condition that exactly 1 or 3 literals must evaluate to 1.
3
votes
1answer
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 ...
2
votes
1answer
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, ...
0
votes
0answers
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. ...
1
vote
1answer
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 ...
0
votes
0answers
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 ...
0
votes
1answer
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 ...
1
vote
0answers
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 ...
2
votes
1answer
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 ...
1
vote
1answer
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 ...
2
votes
1answer
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 ...
1
vote
0answers
99 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 ...
1
vote
1answer
56 views

Not satisfiable 3SAT instance implications

Suppose we have an instance of 3SAT that is NOT satisfiable and we say $S$. If in $S$ there are the following $8$ clauses $\left(a\vee b\vee c\right)\wedge\left(a\vee\bar{b}\vee c\right)\wedge\left(a\...
0
votes
0answers
49 views

Can anyone explain the pigeon-hole encoding method in proportional logic

Someone there who worked with cardinal contraindications within the framework of propositional logic? I have a problem understanding the pigeon-hole method. It is a method of satisfaction. I have been ...
0
votes
0answers
59 views

IF satisfiability problem belonged to P, can the certificate be found efficiently?

IF SAT(satisfiability problem) belongs to P, then is it possible for a certificate of an arbitrary instance of SAT to be found efficiently?
1
vote
0answers
104 views

Reduction between Parity-SAT and approximate counting

Consider two problems as defined here. Approximate counting: Given a Boolean function $f(x)$, for $x \in \{0, 1\}^{n}$, distinguish between the two cases: The number of satisfying assignments for $f(...

1
2 3 4 5
12