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
3
votes
1answer
44 views

Are SAT problems with at most one false clause NP-complete?

Is the problem of deciding whether a SAT instance, where at most one clause is false (that is, any given variable assignment will either lead to all clauses being true, or all but one), is satisfiable ...
1
vote
1answer
47 views

How to encode reachability in a graph with walls as a SAT problem

Suppose we have a graph that represents a grid of cells. We are given a cell to start in and a cell that's the destination. There are cells that we cannot enter and they are known as walls. Finally we ...
2
votes
1answer
47 views

Practical hard 3-sat instances

The $3-SAT$ problem is known to be NP-complete problem. Which means that (as far as I understand), unless $P \neq NP$, for every algorithm $A$ which decides $3-SAT$, $A$ runs in super polynomial time (...
-1
votes
2answers
62 views

A question about NP and coNP

It is an open question if NP $\neq$ Co-NP but if the conjecture were proved, this would mean that P $\neq$ NP because P is closed under complement. Now a fact that fails to enter my head is the ...
1
vote
0answers
36 views

Min-Ones-2-SAT getting to vertex cover

In the Min-Ones-2-SAT problem, we are given a 2-CNF formula φ and an integer k, and the objective is to decide whether there exists a satisfying assignment for φ with at most k variables set to true....
1
vote
1answer
21 views

Is inverse CNF polynomial?

Suppose we are given a CNF formula $F$ with $n$ variables and $m$ clauses. The question is whether we can represent $\lnot F$ as a CNF formula with the number of clauses polynomial in $n$ and $m$?
7
votes
1answer
599 views

Random restarts for unsatisfiable instances

In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice. ...
1
vote
1answer
28 views

Is properly quantified 3SAT complete for PSPACE and all PH levels?

I know 3SAT is NP-complete and QSAT is PSPACE-complete. However, is it true that $$\exists X_1 \forall X_2 \cdots Q_k X_k \colon \varphi(X_1, \ldots, X_k)$$ is complete for $\Sigma_k$, the ...
3
votes
0answers
59 views

High-dimensional geometry and P vs. NP

Background: Recently, I obtained the following equivalent problem to SAT. We are given as input a CNF formula with $n$ variables and $m$ clauses. Suppose we have an $n$-dimensional hyper-cube centered ...
0
votes
2answers
27 views

Does the naive conversion of a Boolean Formula to CNF have a polynomial or exponential complexity?

I am reading the naive conversion to CNF, this procedure is explaining in this book book, but I have not found a conplexity analysis of this algorithm: elimination of equivalence Elimination of ...
2
votes
1answer
33 views

CLIQUE $\leq_p$ SAT

i'm trying to reduce CLIQUE to SAT: Given: Graph G=(Vertices V, Edges E) and $k \in \mathbb{N}$ Output: Formular F such that if G contains a complete subgraph of size k, the formular is satisfiable (...
0
votes
1answer
49 views

A doubt on converting NOT gate to CNF formula

For a NOT gate if $x_1$ is input and $x_2$ is the corresponding output, I see the equivalent CNF (conjunctive normal form) is $(x_1 \lor x_2) \land (\overline x_1 \lor \overline x_2)$. My ...
2
votes
0answers
120 views

Second Order QBF

Consider a universe with two elements 0,1 and a second order formula, i.e. of the form "forall R exists S ... such that F", where R,S are relation symbols of some given arity, and F is some first ...
0
votes
1answer
30 views

Encoding a “not-k-out-of-n” constraint for SAT solvers

I'm finding myself needing to encode a "not-k-out-of-n" constraint in a SAT solver. The "at-most-k-out-of-n" constraint for SAT solvers is something I can find research about -- this paper by Frisch ...
3
votes
0answers
55 views

Determine if a graph has exactly 1 cycle using a SAT solver

I have a connected undirected graph whose edges are either enabled or disabled. I want to create a set of clauses that are SAT iff all enabled edges are part of a single loop. If I assert that each ...
5
votes
1answer
301 views

SAT algorithm for determining if a graph is disjoint

What are some good algorithms to have a SAT (CNF) solver determine if a given graph is fully-connected or disjoint? The best one I can think of is this: Number the nodes 1..N, where N is the number ...
0
votes
2answers
131 views

Reducing Graph Reachability to SAT (CNF)

So I came across this problem in my textbook. I was wondering how to develop a reduction from the Graph Reachability problem to SAT (CNF) problem. (i.e. formula is satisfiable iff there exists a path ...
2
votes
2answers
58 views

Prove that this language is NP-Hard

Given $$\mathrm{\#3SAT} = \{ (w, y) \mid w\text{ is a $\mathrm{3SAT}$ instance with at least $y$ satisfying assignments}\}\,,$$ prove that $\mathrm{\#3SAT}$ is NP-Hard. I am currently stuck with ...
4
votes
0answers
76 views

What is the generating algorithm for the “komb” instances found on satcompetition.org?

For the 2017 and 2018 Random SAT Tracks of the SAT Competition ran by the International Conference on Theory and Applications of Satisfiability Testing there are small, yet difficult, random 3-SAT ...
4
votes
2answers
70 views

Can every Turing Machine be translated into a SAT formula?

For the proof of "Cook-Levin Theorem", for a Turing Machine $M$ that accepts a language $L \in NP$ and input $x \in \{0,1\}^*$, we can create a SAT Formula, that is satisfiable if and only if $M$ ...
3
votes
0answers
32 views

Is there a correspondence of steps between DPLL and sequent-calculus?

Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid? And given ...
1
vote
2answers
114 views

Reduce 4-SAT to 5-SAT

given is a reduction from 4-SAT to 5-SAT. How is it possible to describe such a function? I found some informations about reduction 3-SAT to 4-SAT here, but it can't help me so much.
0
votes
0answers
28 views

Is retrospective inference NP-hard?

Here is a minimal working example of the question: Consider a network with nodes arranged in a pyramid: $1$ node in the first row, $1+d$ nodes in the second, $1+2d$ nodes in the third, and so on, ...
2
votes
0answers
41 views

Is a “stacked”, “local” version of 3-SAT NP-hard?

In this previous question, I learned that if each variable in a string $C \in 3\text{-SAT}$ appears only "locally", then finding a satisfying assignment is no longer NP-hard. My question below builds ...
2
votes
1answer
33 views

Translation of diagnosis problem to SAT

I have the following diagnosis problem: h(A): z1 = not(in1) h(D): z2 = not(in2) h(B): z3 = z1 or z2 h(C): out1 = not(z3) h(E): out2 = not(z3) This is an image of the system: I have an observation ...
7
votes
1answer
403 views

Is a “local” version of 3-SAT NP-hard?

Below is my simplification of part of a larger research project on spatial Bayesian networks: Say a variable is "$k$-local" in a string $C \in 3\text{-CNF}$ if there are fewer than $k$ clauses ...
3
votes
1answer
34 views

Finding a language that is $NP^L$-complete

I'm trying to prove a theorem and as a lemma I would like to identify an $NP^L$-complete language. I was thinking something like a machine that can decide $SAT$ equipped with an oracle for $L$ can ...
4
votes
3answers
412 views

Showing that HALF-2-SAT is in P

I need to show that the following problem is in P: $$\begin{align*}\text{HALF-2-SAT} = \{ \langle \varphi \rangle \mid \, &\text{$\varphi$ is a 2-CNF formula and there exists an assignment} \\ &...
2
votes
1answer
24 views

Satisfiability Toward A Sequential Circuit

Define a sequential circuit model be a directed graph with each vertices being a boolean gate. The difference is that we allow cycles in the boolean circuit. Each cycle will determine a boolean ...
4
votes
1answer
56 views

MAXSAT approximation

We have been studying a 1/2-approximation for MAXSAT which runs in expected polynomial time, by randomly assigning True/False to each variable and repeating until we reach an assignment with at least ...
0
votes
0answers
22 views

What would be a good way to prove NP-Completeness of Min-satisfiablity problem

I am trying to prove the NP-Completeness of Min-satisfiability problem which can be defined as: Given a CNF formula (Set of clauses of 1 or more boolean variables) and a number x, there exists a ...
1
vote
1answer
78 views

3-DNF proves the algorithm is in P class

To understand fully, please read link After, reading the link we will take a look at how we recover our solutions to a constrained Sudoku Puzzle. If we assume that a sudoku puzzle was generated with ...
2
votes
2answers
96 views

Proof that POSITIVE-3-SAT is in the complexity class P

I have the following language: $$\text{POSITIVE-3-SAT} = \{\langle\phi\rangle \mid \phi\text{ is a satisfiable boolean formula in conjunctive normal form,}\\ \text{ in which all clauses consist of ...
8
votes
2answers
2k views

Is “Reachable Object” really an NP-complete problem?

I was reading this paper where the authors explain Theorem 1, which states "Reachable Object" (as defined in the paper) is NP-complete. However, they prove the reduction only in one direction, i.e. ...
1
vote
0answers
129 views

Can someone give me the resolution procedure for 2 SAT, which is O (nˆ2)

According to Wikipedia, Even, S .; Itai, A .; Shamir, A. cited it in "On the complexity of time table and multi-commodity flow problems". The paper can be found here: http://www.cs.technion.ac.il/...
0
votes
1answer
48 views

Resolution when clauses contain more than 1 complementary literals

Let's assume that we have clauses $(l_1 \lor l_2 \lor l_3), (\neg l_1 \lor \neg l_2 \lor l_4), (l_1 \lor l_2 \lor l_5), (\neg l_1 \lor \neg l_2 \lor l_6)$, where both $l_1$ and $l_2$ are complementary ...
0
votes
1answer
25 views

Can someone give me the definition of #Monotone-2SAT?

In the decision problem, I set all variables to true and see if the formula is satisfiable. My question is because I do not understand how there can be multiple solutions, though all variables are ...
1
vote
0answers
61 views

The NP completeness proof for a variation of the 3CNF-SAT problem

There is a variation of 3CNF-SAT which is called 10-3-CNF-SAT = {<$\Phi$>: $\Phi$ is a satisfiable CNF formula with $\textbf{at most}$ 3 literals per clause and every variable occurs in $\textbf{at ...
0
votes
2answers
79 views

Why is Boolean satisfiability such a rare case?

In the space of all K-sat formulas, True and False should have an equal set size. For every un-Satisfiable formula (F), there will an F' (or F-prime) which will be Satisfiable by definition. I cannot ...
3
votes
2answers
95 views

Is every X3SAT instance with no cycles satisfiable?

Exactly 1 in 3 SAT (X3SAT) is a variation of the Boolean Satisfiability problem. Given a set of clauses, where each clause has three literals, is there an assignment such that in each clause exactly ...
1
vote
1answer
75 views

Counting models satisfying a boolean formula

I'm trying to implement the #2-SAT algorithm from the paper "Counting Satisfying Assignments in 2-SAT and 3-SAT" (Dahllöf, Jonsson and Wahlström, Theor. Comput. Sci. 332(1–3):265–...
1
vote
2answers
40 views

Can problems of class P be transformed into SAT formula?

I know that NP problems can be transformed into SAT (due to this fact, SAT is considered to be a NP Complete problem). I am not sure if P problems can too be transformed into SAT.
0
votes
1answer
44 views

Fine-grained complexity of 3-CNF formula evaluation

It's well known that 3-SAT is in NP, which means that one can evaluate a 3-CNF formula in polynomial time. However, I was wondering what the tightest upper bound is for formula verification, expressed ...
2
votes
2answers
47 views

Calculating the number of assignments satisfying a general propositional formula

I know, for a disjunctive clause of the form $x_1 \vee ... \vee x_i$, the number of assignments satisfying it is simply $2^i - 1$, but what about for a general formula? Is the number of satisfying ...
1
vote
1answer
17 views

For a given k-DNF formula, what is the size of the formula for the purpose of complexity?

I am currently in the process of proving some complexity bounds about k-DNF. However I am confused what the $n$ in the time complexity would refer to in this case (that is that I don't know how the "...
1
vote
0answers
54 views

Can I use the Quine-McCluskey to simplify a CNF which is not a product of maxterms?

As I understand it the Quine-McCluskey method allows you to start with a set of maxterms (or minterms), and combine them pairwise in a systematic way into a smaller set of clauses with a smaller set ...
3
votes
1answer
40 views

Refutation in first order logic

Consider the following statement In FOL, we can reduce entailment checking to satisfiability checking: $S \models S' \iff S \land \neg S'$ is satisfiable (This proof strategy is called ...
1
vote
1answer
89 views

Why Cook-Levin thorem's proof can mean SAT's NP-Hardness

I'm studying about Cook-Levin theorem but there is a problem I faced. Cook-Levin theorem shows that any NPTM can be encoded as a boolean formula. About given language $A$, instance $w$, and NPTM $M$ ...
3
votes
0answers
57 views

relationship between SAT and Min-ones SAT

If SAT can be decided in polynomial time, is it clear that Min-ones SAT can be decided in polynomial time? The idea I had was to take a poly decider of SAT and try it on a formula OR'd with all ...
0
votes
2answers
112 views

Seeking nontrivial small SAT/UNSAT instances

I need SAT instances, involving 9 to 20 variables. They need to be hard to solve for humans. Both SAT and UNSAT instances are needed. I tried random-SAT generators on the web, but the results were ...