Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
423
questions
1
vote
1answer
22 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
60 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
49 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
48 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
63 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
29 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
30 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
135 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
77 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
72 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
115 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
415 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
57 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
49 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 ...
