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
8 views

Computational Complexity of Not All Equal Variant with additional constraints

Given an instance of 3-SAT with N clauses and N variables. This problem is NP-Complete. Now, let us consider a restricted version of 3SAT: For each clause $x+y+z=1$ there exists a clause $\lnot x + \...
0
votes
0answers
24 views

Polynomial reduction to SAT with a condition

Let L be in NP. Is there always a reduction from L to SAT where atleast m-1 clauses (m being the number of clauses in the CNF formula) can be satisfied? When w is in L it is trivial because the ...
0
votes
0answers
20 views

Understanding Theory of DPLL [closed]

I have several questions regarding DPLL Algorithm : Does by doing BCP could expose a new pure literal? Does by doing PLP could expose a new unit propagation? Can the output of DPLL is correct if we ...
0
votes
1answer
37 views

Can 3-SAT be recognized in less than exponential time?

Obviously it is an open question if $3$-SAT can be decided in a polynomial amount of time. But what results do we know about its recognizabilty? Can $3$-SAT be recognized in a polynomial amount of ...
1
vote
0answers
23 views

Conflict Clusters – Another P=NP Proof [closed]

Conflict Clusters – Another P=NP Proof Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiability problem. Given an instance of clauses where each clause has three literals, is there a ...
2
votes
1answer
27 views

Reducing a CNF formula to a DNF formula in less than exponential time

The easy way is by looking at the $\{0,1\}$-table and construct the corresponding DNF formula from that, but this will take $2^n$ time. I want to do it much more efficiently. My idea is based upon the ...
3
votes
1answer
38 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 ...
4
votes
1answer
68 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 (...
2
votes
1answer
28 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
1answer
24 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-...
2
votes
0answers
32 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 ...
6
votes
1answer
119 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$, ...
2
votes
1answer
35 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 ...
3
votes
1answer
88 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 ...
2
votes
1answer
31 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 ...
2
votes
3answers
129 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 ...
0
votes
3answers
40 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 ...
0
votes
1answer
35 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
1answer
74 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 ...
3
votes
1answer
125 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
32 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
60 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
201 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
43 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
470 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
26 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
58 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 ...
3
votes
1answer
83 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
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 ...
2
votes
1answer
64 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
87 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
59 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
34 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
71 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
128 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
26 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
120 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
28 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
55 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-...
3
votes
1answer
111 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
56 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
59 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
50 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
37 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 ...
3
votes
1answer
128 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
30 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
53 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
90 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
54 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
71 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
2 3 4 5
12