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

2
votes
1answer
25 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
29 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
42 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
47 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
31 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
27 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
36 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
67 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
32 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
37 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
54 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
44 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
68 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
53 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
61 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
57 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
42 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
25 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
70 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
140 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
49 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
42 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
41 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
50 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| ...
0
votes
0answers
98 views

Converting a boolean expression into CNF and DNF

Is there any systematic way to convert the following boolean expression (QUBO) into CNF or DNF? Here, $x_1, \ldots, x_n \in \{0, 1\}$, $a_1, \ldots, a_n \in \mathbb{Z}$ and $b_{1,1}, \ldots, b_{n,n} ...
4
votes
2answers
115 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
55 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
0answers
36 views

pseudo-boolean optimization or max-SAT

I get very confused about the definition of pseudo-boolean optimization: Firstly, from this paper: rutcor.rutgers.edu/~boros/Papers/2002-DAM-BH.pdf it is defined the same as this wiki (minimizing a ...
0
votes
2answers
35 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
26 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
31 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
33 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
35 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
116 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 ...
1
vote
0answers
87 views

How to minimise an objective function which is not a direct function of the decision variable?

I have a problem with partitioning a water network by closing some pipes. I use some graph theory techniques to find some candidate pipes to close; but to select which pipes among them to close (my ...
0
votes
1answer
60 views

How to give an assignment of boolean values such that this expression is evaluated to true?

Given the expression $E$, is there an assignment of boolean values ($true$ or $false$) that we can give to our variables such that this is evaluated to $true$? $E = (¬x + z + ¬v) · (¬v + w) ·(¬z + ...
1
vote
1answer
87 views

Convert 4-sat to 3-sat

I want to know in general how can I convert $4-SAT$ to 3-SAT. And I have a specific case that if you can help me optimize it to 3-SAT it will be greate. I want to do this so I be able to use sat ...
0
votes
1answer
93 views

What is SAT in mathematics? [closed]

What is SAT, SAT-Solvers and propositional reasoning? I heard a lot about these terms but never worked closely. Looking for someone to explain these terms in easy language with simple example(s).
0
votes
1answer
71 views

2 Sat proof with conjectures

I am trying to convert the following conjectures to implications to then draw the implication graph. The conjectures are: ...
2
votes
1answer
368 views

Converting 2 sat formula into an implication graph.

Both wikipedia and my lecturer explained how the 2 satisfiability problem work. However, I am finding it really hard understanding how this formula: ...
0
votes
1answer
51 views

Question regarding wffs sets, and satisfiability.

Let A and B be satisfiable (in the way the term is used in mathematical logic, with wffs, etc.). How do I show that the union and intersection of A and B are both also satisfiable? I'm slightly ...
1
vote
1answer
73 views

How to find if a valuation satisfies a statement?

I'm working on a task which i'm a bit stuck at. I need to decide whether the statements are true or fale. F stands for the statement logical formulas, and also if the claim is true I need to give a ...
0
votes
2answers
136 views

Resolution on 3-SAT instance yields in polynomial many resolvents

A SAT instance in CNF with $n$ variables has at most $2^n$ resolvents, therefore the resolution method is not in polynomial time. Considering a 3-SAT instance, we have at most $n^3 + n^2 + n$ many ...
1
vote
1answer
152 views

$\Sigma_k^\text{P}$−SAT definition is not clear to me

I don't understand if by saying there are $k$ alternating quantifiers on the variables $x_1$,$x_2$...$x_k$, It means we quantify ALL variables (there are only $k$ variables in the SAT formula) or just ...
1
vote
0answers
82 views

Simplify Fibonacci Power Series

I am working on an algorithm to count the number of models for Exactly One in Three SAT (X3SAT) instances. It is known that a chain of X3SAT clauses of length $c$ has $F(c+3)$ satisfying assignments ...
6
votes
2answers
207 views

Can SAT instances be solved using cellular automata?

I'm a high school student, and I have to write a 4000-word research paper on mathematics (as part of the IB Diploma Programme). Among my potential topics were cellular automata and the Boolean ...
2
votes
2answers
284 views

Proving non satisfiability of the barbers paradox with tableau method

The barbers paradox: In a town there is only one barber. For every man in town, either the barber shaves him or he shaves him self. I need to formalize this: The barber shaves exactely those who ...
1
vote
0answers
137 views

Prove that a problem is NP-Complete with a reduction from 3-SAT

Here is an instance of a problem: Instance: {U, S1, . . . Sn, k|U is a set of elements, the Si are different subsets of U, and k is a nonnegative integer}. A YES instance is defined as follows: There ...