For questions on the subject of "satisfiability", that is, whether there exists an interpretation/model in which a given (logical) formula is true.

learn more… | top users | synonyms

0
votes
1answer
12 views

Simplifying DNF conversion?

Context: I have a huge circuit with lots of input bits (around 300). Among these, only about 40 are free, the others are fixed by the current state. I have to find all satisfying assignments knowing ...
0
votes
2answers
44 views

threshold for random 2-sat

I'm looking at notes on the threshold for random 2-sat which is given as $r_{2}^{*}=1$. In the first part of proving the threshold they claim that a 2-sat formula is satisfiable if and only if the ...
0
votes
0answers
2 views

Strahler Number with empty clause

Definition: The space of an unsatisfiable CNF formula $\Gamma$, noted $s(\Gamma)$, is equal to the minimum among all Strahlers of tree-like refutations of the formula. I am need to proof that ...
0
votes
0answers
9 views

How exactly does a Max 2 Sat reduce to a 3 Sat?

Note: I've also asked this question on StackOverflow here I've been reading this article which tries and explains how the max 2 sat problem is essentially a 3-sat problem and is NP-hard. However, if ...
1
vote
1answer
32 views

Logic - Proving or disproving a formula is satisfiable

I want to find out if the formula $\{p\implies(q\land r),(p\lor r)\implies q,\neg r\}$ is satisfiable. (meanings each clause is satisfiable. there is an $\land$ between the clauses. The problem is ...
0
votes
1answer
41 views

How to decide whether a logical formula is satisfiable

I'm trying to solve one logical problem. I have Language L={P} with equality (there can be '='). And we have 4 formulas an theories of this language. We have to ...
0
votes
0answers
29 views

What is the definition of Planar $3$-Sat problem?

I have some steps in my lecture-notes to make an instance of Planar $3$-Sat problem from an instance of $3$-Sat problem. The steps are as follows: Create one vertex for every literal $x_i$ Create ...
2
votes
1answer
23 views

A query about reducting SAT to 3SAT when there are more than 3 literals in a clause

$C=a∨b∨c∨d∨e$ is a clause in SAT $D= (a∨b∨x)∧ (¯x∨c∨y)∧ (¯y∨d∨e)$ is the another form of C to make sure every clause has only threeliterals Is D true when C is true and false when C is false? Why? ...
0
votes
1answer
24 views

Why is this clause unsatisfiable?

The question says, Which of the following statements apply? And the answer says this one does but I'm not sure why. The clauses {a,b},{a,-b},{-a} are unsatisfiable The clauses {a},{-a,b},{-b} are ...
0
votes
0answers
22 views

SAT and NAE-SAT

Describe a polynomial-time transformation TRAN that takes an instance of SAT and transforms it into an instance of NAE-SAT (the problem where, given a Boolean expression in CNF form, you are asked, ...
0
votes
0answers
32 views

Prof involving completeness of the tree method

I'm working my way through the proof above, and would just like some feedback as to whether my proposed proof is complete. I think I've got everything, but I just wanted to make sure. I'm preparing ...
1
vote
1answer
296 views

proving the validity

I need to prove the validity of the formula: $Q= \forall x \forall y \forall v \ F(x,y,f(x,y),v, g(x,y,v)) \rightarrow \forall x \forall y \exists z \forall v \exists u \ F(x,y,z,v,u)$ I thought the ...
1
vote
1answer
33 views

How to Solve this Boolean Equations?

I have a Boolean Equations, described as below, $$\neg \mathbf{x} = \mathbf{M}\cdot \neg(\mathbf{M} \cdot \mathbf{x})$$ in which $\mathbf{M}$ is an $n\times n$ Boolean matrix, and $\mathbf{x}$ is an ...
0
votes
0answers
46 views

How to Solve Boolean Matrix System?

I have a Boolean Matrix System (BMS) as described below $$Ax=c$$ where $A$ is a $n\times n$ Boolean matrix (i.e., all entries are either 0 or 1), $c$ and $x$ are two $n$-dimensional Boolean column ...
2
votes
1answer
16 views

Showing a reduction between decision problems

I asked a similar question on cs.stackexchange, but I'd like to ask it a tad more specifically, and thought this would be a better place for it. I'm looking through a text on logic, and the problem is ...
1
vote
0answers
40 views

how to determine if formula satisfies without creating a truth table

$(p \wedge q \wedge r) \wedge (\neg p \vee r)$ So far, what I have got is that $(p \wedge q \wedge r)$ satisfies because if $p$, $q$ and $r = 1$ then $(p \wedge q \wedge r)$ also $= 1$. For $(\neg p ...
2
votes
1answer
34 views

Can CNF Hamiltonian graphs be turned to “DNF” graphs?

Given a CNF SAT formula, we can turn it into a Hamiltonian graph, which is Hamiltonian iff the formula is satisfiable. Now, we can transform the CNF formula into a DNF one. My question is, can the ...
0
votes
1answer
42 views

Lower bound on circuit size of a Boolean function

I'm currently reading a proof of the following claim from the notes http://www.cs.berkeley.edu/~sinclair/cs271/n5.pdf which can be found on the bottom of page 6. I'd like to point out i'm interested ...
-1
votes
1answer
94 views

Proving unsatisfiability with propositional resolution

I'm having trouble understanding how to use the resolution rule to prove if a statement is satisfiable or unsatisfiable. I watched this course lecture on propositional resolution and unsatisfiability ...
-1
votes
1answer
81 views

How to reason with Equisatisfiability

I am having trouble reasoning about the equisatisfiability of statements. (In the following I'll use the notation where addition is OR, multiplication is AND, and overbar is NOT.) By exhaustive ...
2
votes
0answers
40 views

Symbolically formulate the two guard problem so it can be solved by a computer

Take the classic two guard riddle (I don't know where the origin of this riddle is, so I'll take the version from http://www.calpoly.edu/~mcarlton/riddles.html): You stand at a fork in the road. ...
0
votes
0answers
39 views

Complexity of computing a posiform of a quadratic pseudo-boolean function

I am reading the chapter 13, Pseudo-Boolean functions, of Boolean Functions: Theory, Algorithms, and Applications by Crama et. al. In section 13.2, the authors introduce the idea of Posiform. The ...
2
votes
1answer
45 views

If $\Sigma$ is finitely satisfiable, can both $\Sigma \cup \{ \phi\}$ and $\Sigma \cup \{ \neg \phi\}$ be finitely satisfiable?

In propositional logic, if $\Sigma$ is finitely satisfiable, can both $\Sigma \cup \{ \phi\}$ and $\Sigma \cup \{ \neg \phi\}$ be finitely satisfiable? I proved that at least one of $\Sigma \cup \{ ...
0
votes
1answer
223 views

reduction from 3sat to 3 dimensional matching.

I've been reading about the standard reduction from 3sat to 3DM and my question was regarding the 'clean up gadgets'. So suppose i take an instance of 3-Sat with $n$ variables and $k$ clauses. Once we ...
2
votes
1answer
41 views

Is $P^{SAT}$ equal to NP $\cup$ co-NP?

I have following problem: Is $P$ with a $SAT$ oracle equal to $NP \cup coNP$ assuming that $NP \neq co-NP \neq P $? I can show that $NP \subseteq P^{SAT}$ and $coNP \subseteq P^{SAT}$. But it is much ...
0
votes
1answer
83 views

Rule of inference - Biconditional proposition

I'm having trouble with one of the questions given as an assignment which is to prove: $$(p\land q)\leftrightarrow(r\land s), \neg r\land q \vdash \neg p$$ I guess I should use proof by ...
2
votes
1answer
66 views

What is satisfiable by a reduct of a model is satisfiable by the original model (and vice versa)?

My professor told me that any formula that is satisfiable by a reduct of a model is satisfiable by the model it is a reduct of, and vice versa (as long as the formula is interpretable on the ...
0
votes
0answers
48 views

Proof by contradiction that $P \rightarrow Q$ is true

Let $\tau$ be a closed tableau. Prove that $\tau$ is not satisfiable. So let's say the statement can be expressed by $P \rightarrow Q$. To prove that this statement is true, we look at the assumption ...
0
votes
0answers
48 views

Non Satisfiability of disjuction

Problem: If S1,S2 are (possibly infinite) sets of propositional formulas where their union: S1VS2 is not satisfiable, prove that there exists an ψ such that S1|=ψ and S2|=¬ψ. Can we say that if ...
1
vote
1answer
73 views

Let $\tau$ be a closed tableau. Prove that $\tau$ is not satisfiable.

Let $\tau$ be a closed tableau. Prove that $\tau$ is not satisfiable. Okay can prove this by contradiction. So we say that a tableau $\tau$ is $\textit{satisfiable}$ iff there exists an ...
0
votes
0answers
57 views

Interpretation and truth table is enough to showing validity or a better way?

I'm so glad that find this useful site. anyway, I ran into some challenging ways to find a formula is valid. Here is two example in my note that called valid. I ran into such a problem with making ...
0
votes
1answer
64 views

Let $\tau$ and $\rho$ be tableaus such that $\tau \leadsto \rho$. Prove that $\tau$ is satisfiable if and only if $\rho$ is satisfiable.

I have this definition: Let $\nu$ be any propositional interpretation. Let $b$ be any branch of a tableau. Say that $\nu$ is faithful to b if and only if for every formula, $A$, on the branch, ...
1
vote
0answers
191 views

How to convert conjunction inside disjunction into CNF?

How do I convert something like $$\bigvee_{a\in A} \bigwedge_{i\in L} (x_{i,a} \wedge y_{i,a})$$ into CNF? The $x_{i,a}$ and $y_{i,a}$ are variables.
0
votes
0answers
53 views

Proving that a set is not negation complete

I'm working through an exercise which involves negation completeness. Let $S = \{R\}$. Let x and y be distinct variables. Suppose we have the set $\phi = \{Rx \vee Ry\}$. Show "Not $\phi \vdash Rx$" ...
1
vote
1answer
33 views

Proof of Satisfiability

I'm learning about the satisfiability of consistent sets and I'm having trouble approaching an exercise. Let $S := \{R\}$ with unary $R$ and let $\phi := \{\exists x\,Rx\} \cup\{\neg Ry \mid y\text{ ...
0
votes
2answers
130 views

Satisfying assignments, twice-3SAT NP complete

I wanted to solve the following problem about 3SAT . The question is 1. to show if the problem is NP-complete and 2. whether the problem has two different satisfying assignments. "TWICE-3SAT Input: ...
0
votes
1answer
486 views

Reduce Hamiltonian Path to CNF SAT

I'm trying to figure out how to reduce a 5 vertex graph to a Boolean equation that will answer if the graph contains a Hamiltonian path. For a Hamiltonian Path to be present in a graph: Each vertex ...
2
votes
1answer
53 views

Prove $\forall z\left(\left(\exists xA\rightarrow A_{x}[z]\right)\rightarrow B\right)\vDash B$

I'm doing some self-exercises on mathematical logic by myself and have come across this question which I can't seem to prove: Let $A$ be a formula with a single free variable $x$. Let $B$ be a ...
0
votes
1answer
45 views

Computational tree logic satisfiability.

In the model I pasted above where $S_0$ and $S_1$ are starting states, is the $EXp$ formula satisfiable? $$M,s\vDash EXp$$ Does it have to be satisfiable for all the starting states given the $M$, ...
0
votes
1answer
58 views

How many satisfying assignments are there in a set of 3-CNF clauses where no clause share the same variable?

Say I have a set of 3-CNF clauses $$\mathcal{S} = \{ x_1 \vee x_2 \vee \bar{x_3}, ~~x_4 \vee x_5 \vee x_6\}$$ where $\bar{x}$ is the negation of $x$. Each variable range over $\mathbb{Z}^2$. How ...
1
vote
1answer
57 views

Is a subset of a NP-complete language also NP-complete?

For example, we know that $SAT$ is NP-complete. However, what if we have a set $subSAT \subset SAT$. Is $subSAT$ NP-complete? What if we have a set $numSAT$ where $numSAT = \{ x \in SAT \; | \; |x| ...
4
votes
2answers
167 views

Las Vegas algorithm to satisfy most clauses in SAT

Consider an instance of SAT with $m$ clauses, where every clause has exactly $k$ literals. Give a Las Vegas algorithm (i.e., an algorithm that always gives the correct result) that finds an assignment ...
1
vote
1answer
63 views

is $P(x) \to \forall x P(x)$ satisfiable

I need to prove that this formula $P(x) \to \forall x P(x)$ is satisfiable. Can I say for example that x is even number ?
0
votes
2answers
44 views

Logic : unsatisfiable set

It is obvious that for a set $\Phi$ of well-formed formulas, if $\Phi\cup\left\{\alpha\right\}$ is unsatisfiable and $\Phi\cup\left\{\left(\neg\alpha\right)\right\}$ is unsatisfiable, then $\Phi$ ...
1
vote
1answer
32 views

Verfiying satisfiability of formulas

I have this question And was wondering if someone could help improve my answer (I am learning English): a) satisfiable as long P=True, Q=True, R= True. Then (P^Q^R) will be true. Also, (not P or ...
0
votes
0answers
44 views

Expanding a logical expression

I need help understanding the following notation. I tried to expand it and that's where I realized I didn't quite get it. How do you expand the following: $${\underset{i=1}{\stackrel{3}{\bigwedge}}} ...
0
votes
1answer
38 views

List of unsatisfiable cores?

Is there a place I can find a list of known unsatisfiable cores for X variables [no more then 10] in CNF format? Or is there an 'easy' way to find out, say I have 7 variables how many clauses [of the ...
1
vote
1answer
56 views

Check whether a set of formulas entails a wff

Given Γ = {p, p → q, q → ¬p, ¬(r ↔ q)} and α = r ∨ q. I have to check whether Γ |= α for the given Γ and α. My solution - Let V be an arbitrary valuation such that V |= Γ. This implies V |= p and V ...
1
vote
1answer
128 views

Mixed Q horn SAT

I am familiar with Horn formula: Formula whose clauses have atmost one positive literal. I am also familiar with Mixed Horn formula: Formula whose clauses are either 2 CNF or Horn. Question 1: But, ...
0
votes
2answers
40 views

Satisfiablity 2

Im trying to work out whether the following clause is satisfiable: {x, y},{x,¬y},{¬x, y},{¬x,¬y},{x, z},{x,¬z},{y, z},{y,¬z} My basic understanding is to work ...