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
29 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 ...
0
votes
0answers
20 views

Is there a universal constant for size of disjoint clauses in 3-CNF

We are given a 3-CNF formula $\Phi$ on n variables, and a guarantee that at least 1% of $2^n$ possible assignments satisfy all clauses in $\Phi$. Now construct set $S$ of disjoint clauses so that no ...
1
vote
1answer
25 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
7 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} ...
0
votes
0answers
38 views

If one shows that UNIQUE k-SAT is in P, does it imply P=NP?

Valiant & Vazirani proved SAT transforms UNIQUE SAT under randomized probabilistic reductions in polynomial time. Calabro et al showed that UNIQUE k-SAT is as hard as k-SAT. Now the question is, ...
4
votes
2answers
86 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
51 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
3 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
28 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
23 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
23 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
28 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
28 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
99 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
32 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
163 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
65 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
23 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
1answer
57 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
46 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
88 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
63 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
233 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
46 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
62 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
94 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
75 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
192 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
244 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
129 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
446 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
71 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
138 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
129 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
61 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
137 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 ...
2
votes
1answer
404 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
726 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!