All Questions
19 questions
12
votes
1
answer
17k
views
DNF to CNF conversion: Easy or Hard
In relation to the thread Proving that the conversion from CNF to DNF is NP-Hard (and a related Math thread):
How about the other direction, from DNF to CNF? Is it easy or hard?
On Page 2 of this ...
8
votes
1
answer
443
views
How much can we reduce the number of clauses by converting from $k$-SAT to $(k+m)$-SAT?
If we suppose that we start with an instance of $k$-SAT, and try converting the problem to an instance of $(k+m)$-SAT, where there are $(k+m)$ literals per clause, can we guarantee a reduction in the ...
5
votes
1
answer
1k
views
How is verifying whether an assignment satisfies a boolean formula possible in polynomial time?
How can I prove that I can verify whether a boolean assignment of variables $a$ satisfies some boolean formmula $\phi$ in polynomial time?
I know that we can just plug the boolean assignment into the ...
4
votes
1
answer
1k
views
Resolution complexity versus a constrained SAT algorithm
EDIT: ad hoc speed-ups are excluded.
We have the result that propositional resolution requires exponential time. The resolution result uses the proof of the pigeonhole principle as an example of a ...
3
votes
1
answer
854
views
Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?
Definition: A renamable Horn formula is a Boolean formula that can be transformed into a Horn formula by flipping the polarity of every instance of one of more of its variables.
Example:
$\qquad (...
3
votes
1
answer
9k
views
Drawing an implication graph for 2-SAT clauses
I am trying to convert the following 2-sat clauses to implications and then draw the implication graph.
The clauses are: ...
3
votes
1
answer
769
views
How many clauses are required for SAT to be NP-hard in CNF formulas?
It is not hard to see that SAT for a CNF formula with $n$ variables and a constant number of clauses can be solved in polynomial time. On the other hand, it is not hard to see that a CNF formula with $...
2
votes
2
answers
149
views
Equivalence of Krom formulas tractable?
Assume I have two Krom formulas $\psi_1, \psi_2$. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, $\...
1
vote
1
answer
1k
views
What is the complexity of determining whether or not conjunction of positive CNF and negative CNF is satisfiable?
Definitions:
positive CNF is a conjunctive normal form formula, where all literals are positive, i.e. the unary connective ¬ does not exist in the formula.
negative CNF is a conjunctive normal ...
1
vote
2
answers
61
views
Complexity of satisfiability for relational logic on the booleans
I know that propositional satisfiability is NP-complete and that if I add first-order quantifiers I get the complete problems for the polynomial hierarchy and PSPACE. What happens if my formulas are ...
1
vote
1
answer
141
views
Does exist NP language that is Cook Levin deterministic reducible to xor satisfiability in polynomial time?
We say that the language $L$ is Cook Levin deterministic reducible to xor satisfiability in polynomial time if and only if for each word $w\in\Sigma^*:w\in L\iff f(w)\in XORSAT$ where $\Sigma=\{0,1\}$ ...
1
vote
1
answer
219
views
Complexity of 1-in-3 SAT variant with restrictions on "unique" variables per clause
I'm interested in the complexity of a particular variant of 1-in-3 SAT. Assume, as is usual, that clauses are allowed to be of length 1, 2, or 3. Then add the restriction that for any clause of length ...
1
vote
1
answer
120
views
Application of Combinatorics, Logic and computability theory in physical science: Tiling of Wang Tile with proportionality [closed]
The original problem of Domino Tiling and Wang Tile has great theoretical interest on computability theory... However, the great emerging problem on application of Wang Tile in material science and ...
1
vote
0
answers
203
views
Could you show the intractibility of SAT by showing that the number of variables contributing to an arbitrary unsatisfied clause is not constant? [closed]
Preface: This is not an attempted proof at P vs NP
Starting with some CNF Boolean expression ϕ, by the rules of logical disjunction, a clause is only unsatisfied if each of the literals in it are ...
0
votes
1
answer
977
views
How can you check if a 2SAT problem has a bad loop
im trying to figure out why this is true
The clauses {a,b}, {b,~c}, {c,~a} constitute a 2SAT problem with an implication graph without bad loops.
Can someone show me how to illustrate this and ...
0
votes
2
answers
478
views
Is 2QBF in P^NP?
2QBF is the following problem: given a CNF formula $\psi$ on $2n$ variables, determine the truth value of
$$\forall x \in \{0,1\}^n . \exists y \in \{0,1\}^n . \psi(x,y).$$
Question: Is 2QBF in $P^{...
0
votes
1
answer
321
views
Reducing "multiple satisfiability" to normal SAT
I have to prove the NP-completeness of the following set:
QUADRUPLE-SAT:={F is Formula in CNF|F has at least 4 satisfying interpretations}
My idea so far has been to reduce the problem to the normal ...
-1
votes
1
answer
106
views
Equivalence of Horn formulas tractable?
Assume I have two Horn formulas $\phi_1, \phi_2$. Horn formulas are CNF formulas so that each clause has at most one unnegated literal. For example:
$x_1 \wedge (\neg x_1 \vee \neg x_2 \vee x_3 )\...
-4
votes
1
answer
234
views
Why is Mixed Quantified Horn SAT in PSPACE?
I want to prove that Mixed Quantified Horn SAT is a PSPACE-complete problem. I have proved that it is PSPACE-hard. How can I prove that it is in PSPACE?
My study:
To prove QSAT to be in PSPACE: ...