Computer Science

Questions tagged [satisfiability]

Ask Question

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

431 questions
Newest
Active
Bountied
Unanswered
Filter by
Sorted by
Tagged with
-1
votes
0answers
22 views

Under the assumption that $P \neq NP$, prove or disprove the following propositions [closed]

I have problem to point 7 and 8. Let $L1,L2 ∈ \{0,1\}^*$. Under the assumption that $P \neq NP$, prove or disprove the following propositions: $L_{1} ∈ P ⇒ L_1^c ∈ NP$. [FALSE] because with $P \neq ...
0
votes
0answers
19 views

CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P

CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P. I found this solution: We use the method of resolution to take the variables out ...
0
votes
0answers
29 views

CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number of literals, but at most one negated literal} ∈ P

The problem derived from the book of Sipser and the question was already posted (link) with partial comments. Let CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number ...
0
votes
0answers
60 views

Using induction prove that a K-SAT problem is NP-Complete

Using induction on k, how do I prove that the K-SAT problem is NP-complete? On wikipedia, it describes the Cook-Levin theorem to prove that K-SAT is NPC by reducting the K-SAT problem to a circuit-...
3
votes
1answer
17 views

CNF satisfiability with a bound on number of clauses

Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
4
votes
2answers
102 views

Are SAT problems with at most two false clauses NP-complete?

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

Significance of quantifier ordering in quantified boolean formulas (kQBF vs. QBF)

I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e ..." ...
5
votes
2answers
199 views

checking '<' for two binary numbers in a cnf-formula

I want to check whether a arbitrary binary number is less or equal to another binary number in a cnf-formula. I can already construct a formula, which is not in cnf: Lets say n and m are two-digit ...
1
vote
1answer
34 views

Find a truth assignment of 2SAT that has the most number of true variables?

Given a 2SAT instance in CNF where each clause has at most two literals. Let $m$ be the number of clauses and $n$ be the number of variables et let $k$ be a positive number. Question: Is there a ...
4
votes
1answer
99 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
75 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
56 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
73 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
59 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
29 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
606 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
46 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
1answer
75 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
38 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
38 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
54 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
127 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
36 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
66 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
334 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
187 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
63 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
80 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
87 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
35 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
175 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
43 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
409 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
484 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
64 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
84 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
104 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
138 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
60 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
38 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
114 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
81 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
106 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
88 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 2 3 4 5 … 9