Questions tagged [satisfiability]
For questions on the subject of "satisfiability", that is, whether there exists an interpretation/model in which a given (logical) formula is true.
340 questions
0
votes
0
answers
61
views
Sufficient Conditions for the missing Moore Graph
In the study of the missing Moore Graph of order 3250 and degree 57 I have asked myself whether it is sufficient to define it as such:
Going from a root node $r_0$, we reach 57 new nodes $a_1, ... , ...
- 174
2
votes
0
answers
67
views
Why is this probability $o(1)$ as $m \to \infty$ in a proof of a randomized algorithm for solving $k$-CNF ($k$-SAT) ? A mistake in a famous book?
This is about the proof of Lemma 5.13 in the well-renowned book Motwani R, Raghavan P. Randomized Algorithms. Cambridge University Press; 1995. Access with institutional login: link.
(The lemma is in ...
- 21
4
votes
1
answer
169
views
How do solvers find counterexamples to loop invariants without iterating through values?
In formal verification, loop invariants are used to prove correctness across all iterations of a loop. A loop invariant is a property that must hold:
Before the loop starts (initialization),
After ...
- 405
0
votes
0
answers
70
views
Exploring Lower Bound Calculations for Optimality in TSP Solutions Using k-Exchanges
I am currently exploring a mathematical approach to calculating the minimal number of comparisons required to establish the optimality of a solution in combinatorial problems, particularly in the ...
2
votes
0
answers
68
views
Cook-Levin theorem, why is $\phi _{cell}$ necessary?
Something I didnt understand from both my university course, Sipser, and looking online, is why $\phi _{cell}$, the formula in the Cook-Levin theorem (defined below) which checks that each cell is ...
- 33
0
votes
1
answer
188
views
Polynomial time algorithm for 3SAT
I followed from this question.
I am following the book, Theory of Computational Complexity, 2nd Edition Ding-Zhu Du, Ker-I Ko.
I am copying following text from the ...
- 55
0
votes
1
answer
110
views
Is there a deterministic algorithm that operates in time $2^{O(\log^c(n))}$?
I am following the book, Theory of Computational Complexity, 2nd Edition Ding-Zhu Du, Ker-I Ko.
I am copying following text from the book,
Recently an algorithm was ...
- 55
1
vote
0
answers
120
views
Is Monotone QSAT PSPACE Complete?
I've seen that "Monotone" is given a few different definitions w.r.t. SAT, but I'm interested in the more common definition: The SAT problem, where each clause contains only unnegated ...
- 111
0
votes
1
answer
201
views
Polynomial block with Turing machine [closed]
A function $f$ is said to be thinking in an encapsulated linear memory if:
$f(x)$ is a polynomial block (that is, there exists a polynomial $q$ so that $|f(x)|\leq q(|x|)$) for each input $x$.
...
user1408191
0
votes
2
answers
161
views
Simplifying $(p\vee\neg q)\wedge(q\vee\neg r)\wedge(r\vee\neg p)$ [closed]
I recently began learning about compound propositions. How to use a sequence of logical equivalences to simplify
$$(p\vee\neg q)\wedge(q\vee\neg r)\wedge(r\vee\neg p)$$
such that it becomes more ...
- 29
1
vote
0
answers
75
views
Is there a name for the problem of finding unique subsets of a set of sets.
Consider a set of possible attributes $A$. I have a collection of objects $C = \{c_1,c_2,\cdots,c_n\}$, and each object is associated with a subset of attributes from $A$. Is there a name for the ...
- 1,621
2
votes
1
answer
103
views
Last Bits of Proof of the Compactness Theorem in Propositional Logic
I am reading the proof of compactness theorem for the propositional logic and the last part of the proof is left as exercise 2 of section 1.7 in the book by Enderton, A Mathematical Introduction to ...
- 15.7k
0
votes
0
answers
45
views
Satisfiability of certain class of 2-CNF formulae
A propositional formula in conjunctive normal form (from now on abbreviated CNF) is said to be in standard form if there are no pure literals, no duplicated clauses, and no possible resolutions in ...
1
vote
1
answer
129
views
How to use resolution in this formula with XOR? [closed]
Transform the set of causes of the given formula are below:
$\overline{x}\lor y.....(1)$
$\overline{y}\lor x.....(2)$
$\overline{z}\lor w.....(3)$
$\overline{w}\lor z.....(4)$
$\overline{s}\lor \...
user1290851
0
votes
1
answer
82
views
Resolution Exponential Memory Blowup
I'm looking at the Davis-Putnam algorithm. I don't understand how resolution results in an exponential blowup in the size of the formula, since it seems that after each step, the size is reduced.
$(...
