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

1
vote
1answer
72 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
26 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
58 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
43 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
16 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
49 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
38 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
83 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
48 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
115 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
41 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 ...
0
votes
0answers
20 views

How to solve statements which satisfies and statements which are valid? [duplicate]

I know i've posted this one time before, but I didn't get a lot of help so i'm trying again since i'm still stuck at this task. I need to decide whether the statements are true or false. F stands for ...
1
vote
1answer
58 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
83 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
66 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 ...
5
votes
2answers
182 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
213 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
357 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
67 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
123 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
134 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
316 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
588 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!