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
0answers
21 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
26 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 ...
2
votes
1answer
20 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
82 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
0answers
27 views

Independent Sets that are Odd Covers

I am interested in a certain type of independent set I call an "odd cover". A set of vertices is independent if no two vertices in the set are connected with an edge. A set of vertices is an "odd ...
0
votes
2answers
35 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 ...
0
votes
0answers
69 views

NAESAT (Not all equal sat) problem

Given the following NAESAT problem: c3 = {x1,x2}, {x2,x3},{x3,x1} where cn = {x1,x2}, {x2,x3}..{xi,xi+1} What is c4? Well ...
1
vote
0answers
49 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
0answers
21 views

Weighted partial MaxSAT (and MinSAT) with real-valued weights?

Consider the following optimization problem ($\min$-version also of interest): $$ \max_{β\in\{0,1\}^m}\{c'φ(β): ψ(β)=1\} = \max_{\phi\in\{0,1\}^n}\{c'\phi: β\in\{0,1\}^m, \phi=φ(β), ψ(β)=1\},$$ ...
0
votes
0answers
18 views

Translate Inequality to 2-SAT

How to translate Inequality, such as $A<B$ to $2-SAT$. I had an idea comparing the bits of the number but I failed implementing it.
0
votes
1answer
54 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 + ...
0
votes
1answer
40 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
0answers
23 views

Satifiablity of a clause

Im working out wether this clause is satifiable: My understanding of satifiability is when the empty clause cannot be derived like: {x}, {¬ x},{x,y,z,w} I would use the following formula: ...
0
votes
1answer
86 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
53 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: ...
1
vote
1answer
150 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
43 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
59 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
1answer
84 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
150 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
68 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
187 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
220 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
119 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 ...
1
vote
2answers
374 views

Converting each formula into Conjunctive Normal Form?

How hard is it to translate an arbitrary well-formed formula into CNF formula? It seems it can get exponential in some occasions like $(a\wedge b)\vee (c\wedge d)$ is transformed into $(a\vee ...
0
votes
1answer
68 views

software for numerical constraint satisfaction problems

Let $m$ be an even integer greater than $8$. Is there any software I can use to determine for some small $m$ whether the following constraints on $t_0,\ldots,t_{m-1}$ and $w$ have solutions? ...
6
votes
1answer
136 views

Deciding a problem: is it in $NP$, $NPC$ or $P$?

I'd like your help with understanding whether the following problem is in $P$, $NP$, $NPC$. The problem $B$: Input: a $3CNF$ formula which contains more than one clause. output: Can we divide the ...
3
votes
1answer
125 views

Potentially stupid question about the Boolean Satisfaction Problem

So I recently learned about the boolean satisfaction problem in an article that linked it to super mario brothers. Anyways, I was wondering why you can't solve the problem in the following way. ...
0
votes
1answer
60 views

Modelchecking on Automata, $\phi$ not SAT and $\phi \models$ False

Given a formula $\phi$ Is $\phi \models FALSE$ equivalent to $\phi$ not SAT? Or does $\phi \models FALSE$ means that $\phi$ is never $TRUE$ and $\phi$ not SAT means, that there existst at least one ...
4
votes
0answers
136 views

Connect 4 - SAT

My question is about how the Hasbro game Connect4 can be viewed as a SAT problem. My initial guess is that it would actually be QSAT, and that the 'problem' would be something along the lines of: "Is ...
1
vote
1answer
349 views

What does this notation mean? (Satisfiability / set notation)

I am studying a satisfiablity course as a part of my computer science degree. My lecturer introduced some notation without explaining it and I can't seem to find out through Google. Let F be a clause ...
2
votes
1answer
626 views

In Satisfiability, what is the difference between the empty clause and the empty set?

The empty clause is a clause containing no literals and by definition is false. c = {} = F What then is the empty set, and why does it evaluate to true? Thanks!