# 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
96 views

### Finding a minimal set of package versions in a dependency graph with constraints

Suppose you have a dependency graph of "packages" registered in the ecosystem of a given programming language. We can model each package as a tuple ...
1 vote
52 views

### Question about a proof of the existence of unsatisfiable linear k-CNFs for any k

Today I am reading paper Unsatisfiable Linear k-CNFs Exist, for every k by Dominik Scheder, 2007. But I have some problem to understand the proof of Theorem $3.2$. I don't know how to understand the ...
28 views

### How to get the formal model using propositional logic

Input There are three chairs (1,2,3) in the same row. We need to find a seat for three guests (a,b,c). Constraints The first guest does not want to be seated next to the third one (neither left nor ...
143 views

### Why solving #2SAT in polynomial time implies P = NP?

The wikipedia article for #P states that if we have a polynomial-time algorithm for a #P-complete problem, P = NP is true. As #2SAT is #P-complete, this would mean that providing a polynomial-time ...
96 views

### NP-hard $k$-SAT variant with exactly $\ell$ occurrences per variable

For the purpose of this post, let $k$-SAT be SAT with exactly $k$ literals per clause, as opposed to the more common meaning of at most $k$ literals per clause. With the purpose of proving some ...
5k views

### Is SAT an existential question?

Some sources state that an algorithm that solves the SAT problem not only needs to decide whether a given existentially-quantified formula is satisfiable or not, but, additionally, in the case where ...
1 vote
45 views

### Possible to solve a combinatorial game with integer programming?

I recently had the idea that it would be neat if it were possible to make a SAT solver play combinatorial games. To start, I'm trying a relatively simple case of solving single-stack Misère Nim ...
1 vote
108 views

### CNF – satisfy at most a fixed number of clauses

I'm working on this task: Prove that the following problem can be solved in time $2^{k} \cdot \Vert \varphi \Vert^{\mathcal{O}(1)}$: given a boolean formula $\Vert \varphi \Vert$ in CNF, decide ...
1 vote
65 views

### Logical Consequence - Equivalent Assertions

I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
77 views

### Running time of SAT and other EXPTIME algorithms

I need to propose an algorithm for a NP-hard problem. I use dynamic programming which leads to a running time $O(2^s\cdot n^2), s\leq n.$ The algorithm aims to finding a path in a graph $G(V, E)$ (in ...
1 vote
55 views

1 vote
52 views

### Reducing a mixed Boolean expression containing XOR of conjunctions

I know that XOR-SAT can be solved in polynomial time using arithmetic in $F_2$ and Gaussian elimination. I have a set of formula that is of the form  G_i := \oplus_{j=0}^{i} \left ( a_j \land b_{i-j}...
61 views

### Can these variants of SAT/Tautology be actually pretty simple?

There are 8 (very similiar) languages I'd like to discuss here: CNF SAT DNF SAT CNF No-SAT (Existence of a false assignment) DNF No-SAT CNF Tautology DNF Tautology CNF Contradiction DNF Contradiction ...
46 views

### Can you help me find some examples of 3co-SAT for 4 variables?

I've been studying the examples of 3co-SAT recently. It's easy to find an example of one variable. $(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$ Examples of 2 ...
60 views

### Why don't we consider that NP = co-NP while we can reduce Tautology problem into Satisfiability in polynomail time easily?

Let's determine if an expression is tautological or not and let's try this expression: ((a ⊼ b) ∨ c) ↔ (¬a ∨ ¬b ∨ c). We can turn this problem into CIRCUIT-SAT decision problem by asking if the ...
36 views

### CNF-SAT time complexity and input processing

Boolean Satisfiability (CNF-SAT) problem in $n$ variables may contain a CNF formula with $O(2^n)$ clauses in the worst case. My question is: Wouldn't a program reading a CNF formula have to ...
1 vote
93 views

### MSAT and IMSAT problems (restricted versions of SAT)

I was reading about about NP-intermediate problems on Wikipedia and saw the IMSAT problem mentioned over there. There is no Wikipedia page for that problem and they only cite this paper. In the paper ...
1 vote
41 views

### Probability of a randomised algorithm solving SAT

Let WALKSAT be defined as follows: Let $σ$ be a random truth assignment to the vars For $t = 1, 2, . . . , 3n$: ◦ If $\phi$ is satisfied by $σ$, exit the loop ◦ Else, pick an unsatisfied clause $c$ ...
257 views

### Complexity of the (Complete/Assign) 3-SAT problem?

A complete $k$-CNF formula on $n$ variables $(k\le n)$ is a $k$-CNF formula which contains all clauses of width $k$ or lower it implies. Let us define the (Complete/Assign) 3-SAT problem: Given $F$, a ...
90 views

### what does **input** mean for the $3SAT$ question? Is it the number of variables $n$ or the number of clauses $m$

We know that $3SAT \in NP$, and the definition of $NP$ is as follows: $NP$ is the class of languages that have polynomial time verifiers. But I have a question: what does input mean for the $3SAT$ ...
288 views

637 views

61 views

### Quantum Boolean SAT algorithm?

Is there a quantum SAT algorithm, a quantum analogue of the DPLL or CDCL algorithms? Note: I'm not looking for the quantum analogue of the Boolean satisfiability problem (though that would be ...
56 views

### SAT and #SAT in Quantum

Let us look at the two questions that are NP-complete for a classical computer: Given an arbitrary Boolean expression, find an assignment of variables that evaluates the expression to $0$ (SAT). ...
288 views

### Integer/prime factorization to 3 SAT

So essentially as the title says, I just want to understand how its done. I have a light idea from my own research, but its failing at one point, and I feel it maybe due to crucial point missing in my ...
94 views

### How to determine if clause will change the satisfiability of the 3SAT formula?

I have satisfiable 3SAT formula like: (x1 or x2 or x3) and (not x1 or x2 or not x3) and some clause which is not in this formula ...
1 vote
31 views

### Radius Local Search Algortihm for Max-Sat problem approximating ratio

Assume that in classical Local Search algorithm for MAX-SAT we could flip no more than $r \leq n/2$ variables (let's call it $r$-flip) on every iteration. More precise: on every iteration we're ...
44 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
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 ...
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 ...