Questions tagged [satisfiability]
For questions on the subject of "satisfiability", that is, whether there exists an interpretation/model in which a given (logical) formula is true.
322
questions
0
votes
0
answers
16
views
Encoding lexicographic order into CNF
Suppose we have two Boolean vectors, $x$ and $y$, of length $n$. How can I encode $x<_{\text{lex}}y$ into a CNF?
The only Boolean formula I can think of is
$$(\neg x_0\land y_0)\lor\bigvee_{i=1}^{n-...
- 423
-1
votes
0
answers
7
views
How to express the Boolean cardinality constraint to CNF formulas? [closed]
A Boolean cardinality constraint
$$\sum_{j=0}^{n-1}x_j=k,$$
where $x_j$’s are Boolean
variables, and $k$ is a non-negative integer.
How to express the Boolean cardinality constraint to CNF formulas?
1
vote
0
answers
31
views
When we necessarily need monadic second order logic
I am a student of graph theory and recently started learning mathematical logic.
If I am not wrong, any problem in the class Np-Complete can be represented as a SAT formula. As boolean formulas are a ...
- 21
1
vote
1
answer
106
views
Must we define $\mathcal A \models (\varphi \wedge \psi)$ using the word "and"?
I'm learning model theory from Kirby's An Invitation to Model Theory. In a recursive definition of the interpretation of $L$-formulas, he defines $\mathcal A \models (\varphi \wedge \psi)$ to be true ...
- 6,422
0
votes
0
answers
17
views
Can this method of converting strict inequalities to equisatisfiable nonstrict inequalities be generalized from real numbers to the extended reals?
I am working on an implementation of Bruno Dutertre's and Leonardo de Moura's paper "A Fast Linear-Arithmetic Solver for DPLL(T)" for SymPy, an open source python library for symbolic ...
- 11
0
votes
1
answer
46
views
what is the maximal and minimum number of linear equations can be satisfied
Given $\alpha>0$, consider the following system of linear equations of variable $x=(x_1,\cdots,x_n)$ where $x\in\mathbb{R}^n\backslash x_0$. The $x_0$ denotes vectors that all elements are equal. ...
- 139
3
votes
1
answer
130
views
Take a 3-SAT system and compute its symmetry group, what can we say? How does this group relate to satisfiability?
Take for example, the $3$-CNF system:
$$
a \vee b \vee c = 1 \\
d\vee -e \vee f = 1
$$
The symmetry group of the first equation is $S_3 = \langle (x,y) : x, y \in \{a,b,c\}, x\neq y \rangle$ because ...
- 20.8k
3
votes
0
answers
45
views
What's meant by a 'reversible Boolean formula' in this context?
I don't think I understand correctly what it means for a Boolean formula to be reversible. By my current understanding, if a Boolean formula is satisfiable, then there exists a setting of variables ...
- 41
2
votes
1
answer
105
views
Satisfiability in an Heyting algebra implies satisfiability in a Boolean algebra for propositional logic?
Let $\mathcal{L}$ be a propositional language and let $\text{Prop}(\mathcal{L})$ be the set of all the propositions of the language $\mathcal{L}$.
Let $(H,\wedge,\vee,\rightarrow,1,0)$ be an Heyting ...
- 445
4
votes
1
answer
82
views
Why is the problem of proving the existence or nonexistence of an algorithm that efficiently solves SAT equivalent to $P = NP$, explained simply?
I am a high school student trying my luck and self-studying topics in mathematics I find interesting. While reading through a course in Math for Computer Science, I came across the statement that ...
- 41
1
vote
0
answers
14
views
Does quantifier elimination preserve equi-satisfiability or equivalence?
Does quantifier elimination (QE) preserve equi-satisfiability or equivalence?
I always thought it preserves equi-satisfiability (and not equivalence) but in the book [Bradley, Manna], they say both ...
- 247
1
vote
1
answer
33
views
Finding solutions to Boolean satisfaction problems
How hard is it to find a solution to an instance of SAT if we know that the instance is satisfiable?
Clearly, finding a solution to a SAT instance is at least as hard as deciding whether the instance ...
- 755
0
votes
1
answer
39
views
How to perform induction on the number of connectives and quantifiers in a well-formed formula?
I am trying to prove the following proposition from Mendelson's book.
If the free variables (if any) of a well-formed formula $\textbf{B}$
occur in the list $x_{i_1}, \dots, x_{i_k}$ and if the ...
- 1,083
0
votes
2
answers
70
views
How to understand one of the properties of satisfaction of wfs in first-order logic?
Proposition:
If the free variables (if any) of a well-formed formula $\textbf{B}$
occur in the list $x_{i_1}, \dots, x_{i_k}$ and if the sequences $s$
and $s^′$ have the same components in the ${i_{1}...
- 1,083
0
votes
0
answers
22
views
How to use SMT solver to prove model validation
I have a mixed-integer model with some parameters. I also have a set of validation rules telling me if the model is satisfiable. How can I use SMT solver to prove that my validation rules are valid ...
- 143
0
votes
1
answer
36
views
Function Mapping: What does $FunctionName: Domain\rightarrow 2^{something}$ mean?
I hope you are all doing well!
I am taking two courses in theoretical computer science, and in both courses I have come across a notation that I am unfamiliar with. It is of the form: $FunctionName: ...
0
votes
0
answers
25
views
$A=\exists x_1\cdots\exists x_n B$ where $B$ is quantifier-free. Proof that it can be decided algorithmically whether A is satisfiable or not.
It is given a sentence $A = \exists x_1\cdots\exists x_n B$, where $B$ is quantifier-free.
Overall: I have to proof that we can decide algorithmically whether $A$ is satisfiable or not.
A hint was to ...
0
votes
0
answers
21
views
Can satisfiability (2 SAT) indicate whether a bad loop is possible in an implication graph?
I have found that these clauses are satisfiable: {a,b},{b,¬c},{c,¬a}
Can I then assume that a bad loop is not possible? Because I have found that it would be possibel to go from b to b, or would this ...
- 1
0
votes
0
answers
294
views
At least one literal has to be true in order to satisfy a CNF
My question is rather a confusion than a misunderstanding.
Today I was introduced to the SAT problem and to the CNF(orm). And started my assignment in it.
I need to define a method, given a list of ...
- 23
0
votes
1
answer
33
views
2SAT Problem: Is it okay to derive the empty clause in this manner?
If I have: {x,y},{x,z},{y,z},{¬x,¬y},{¬x,¬z},{¬y,¬z}
I can see that through the clause {¬x,¬y}, I will be able to cancel out variables to be left with {z}, however, can I use {¬x,¬z},{¬y,¬z} on {z} to ...
0
votes
0
answers
40
views
Understanding why certain clauses disallow deriving an empty clause and the relationship with satisfiability
If I had these clauses: {x,y,z},{¬x,¬y,¬z},{x,¬y},{¬x,z}. Why is it not possible to derive the empty clause from these by a resolution proof?
Also, is there a relationship between resolution proof and ...
0
votes
0
answers
17
views
CNF Satisfiability with Skolemization
I am studying the topic CNF satisfiability, and I am confused with how we can determine a CNF statements with Skolemization satisfiable or not. For example, CNF with variables x0 x1 x2 x3 x4, ...
- 1
0
votes
1
answer
49
views
Satisfiable formula but false in any structure
Exhibit a formula with no free variables that is satisfiable, but false in any structure whose universe has fewer than three elements.
I've thought about this for a while and I can't think of anything,...
- 143
4
votes
0
answers
194
views
Does a cubic graph polynomial contain the $x_1 x_2 \cdots x_M$ term?
Given a cubic graph $G$ (i.e. a graph where all nodes have degree $3$) with $N$ nodes and $M$ edges, each edge is assigned a variable $x_i$. For each node, we are given $y_i$ which is a polynomial in ...
- 1,762
4
votes
1
answer
78
views
Predicate Logic - Try to prove satisfiability or unsatisfiability first
During my course in logic I encountered this problem:
Determine whether the following set of sentences is satisfiable or not. If not, use natural deduction to prove contradiction.
S = {∃x(R(x, x) ∧ ∀...
- 43
0
votes
0
answers
27
views
Is finding the number of solutions to a NP problem significantly harder than solving it?
I am wondering what is known about the problem of finding the number of solution to a NP-complete problem. We can of course take SAT as an example, it doesn't matter that much. It is clear that this ...
- 5,395
0
votes
0
answers
24
views
Requirement of the Second part of PDL Filtration Lemma
I was reading this filtration lemma of PDL in David Harel's book Dynamic Logic.
The Filtration Lemma:
Let $\kappa = \langle W, \mathcal{R}, V\rangle$ be a Kripke model of PDL and let $u, v\in W$:
(i) ...
1
vote
0
answers
27
views
A CSP on bit vector operations
I've got a CSP which is based on constraining bit vector variables. It is explained below through an example, followed by the full definition. So, what I'm concerned about is if you have some idea if ...
0
votes
1
answer
44
views
At most $k$ contiguous $\mbox{true}$ values in a Boolean array using SAT
Given an integer $k > 0$ and a Boolean array $A$ of length $n$, find a simplified and efficient CNF formula to ensure that there is not more than $k$ contiguous $\mbox{true}$ values in this array. ...
- 1,244
0
votes
1
answer
44
views
Checking NP-completeness of the following problem(s)- Assigning candidates to departments
Suppose we have $n$ candidates from a candidate pool $\{1,2, .., n\}$ and we have $m$ departments. Suppose each department $d$ is considering hiring some $C_d \subseteq \{1, 2, ... n\}$ candidates (...
- 1
1
vote
1
answer
95
views
Is there a method to solve 3SAT problems using loss function?
Loss function seems to be used to solve optimization problems. I assumed that 3SAT problems can be treated as them. I would like to know whether there is a good loss function that is defined by ...
- 15
1
vote
1
answer
42
views
How to solve a max CSP with a set of linear constraints?
Suppose there is a set of $n$ linear constraints $\{a_i^Tx+b_i\le 0\}_{i=1}^n$ with $a_i\in\mathbb{R}^d$, $b_i\in\mathbb{R}$, $x\in\mathbb{R}^d$. How can I find $x^*$ that maximizes $\vert \{i\in [n]\...
- 49
2
votes
0
answers
61
views
Finding the greatest common consequence of two propositional formulas
Given two propositional formulas over a set of literals with AND, OR, and NEGATION, find propositional formulas $\phi_1$, $\phi_2$, and $\theta$, s.t. $\phi_i = \theta \wedge \phi_i^*, \; i=1,2$, and $...
0
votes
1
answer
129
views
Why doesn't Krom's method apply to solving the 3SAT in polynomial time?
In the paper "The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary", Krom suggested a method to solve 2SAT problem.
My understanding is this.
Use ...
- 15
3
votes
1
answer
397
views
$(P∨Q)$ is satisfiable if and only if $(P∨R)∧(Q∨¬R)$ is satisfiable
I came across the following statement:
$(P∨Q)$ is satisfiable if and only if $(P∨R)∧(Q∨¬R)$ is satisfiable
And I am supposed to say whether it is true or false.
Let $F(x,y,z)$ be a boolean function (...
- 777
0
votes
1
answer
69
views
A counter example for $\Gamma\vDash_{v}B\Longleftrightarrow\Gamma\cup\{\neg B\}$ isn't satisfiable by a model
I'm trying to disprove:
$\Gamma\vDash_{v}B\Longleftrightarrow\Gamma\cup\{\neg B\}$ isn't satisfiable by a model (for every assignment).
In first order logic.
where $\vDash_{v}$
means that for every ...
user846115
2
votes
0
answers
57
views
if $Γ\vDash\forall x_{1}...\forall x_{n}\left(\left(\exists yϕ(x_{1}...x_{n},y\right)\leftrightarrowϕ(\frac{t}{y})\right)$ then ψ exists
Let $Γ$ be a set of sentences over a dictionary $\Sigma$. it is known that for any formula $\phi(x_1,...,x_n)$ has logical term t, such that $\text{fv}(t)\subset\{x_1,...x\}$
and $$Γ\vDash\forall x_{1}...
user846115
4
votes
1
answer
147
views
First order logic: if A sentence is satisfiable then it is satisfiable in the natural number + even function
Let $\Sigma=\{R(,),f(),g(,)\}$ and let f,and g be functions, and R a relation in FOL logic without equallity.
Prove or disprove:
if $\phi$ is satisfiable and a universal sentence, then there is a ...
user846115
0
votes
1
answer
29
views
How to find variable sets of such "one valid" property?
Let's assume that we have to solve a 3-SAT instance (encoded in CNF form) and we are looking for sets of N-variables (smaller are better) that has the following property:
When we turn such a set of N-...
- 123
0
votes
2
answers
41
views
Trying to understand 3-SAT self-subsuming process
I've been studying solver theory and am trying to understand some of the basic concepts that I've been reading. In particular, the idea of self-subsuming (if I have the correct terminology here) is ...
5
votes
2
answers
243
views
Kees Doets's definitions of logical consequence
everyone, I'm reading Kees Doets's Basic Model Theory (which is freely and legally downloadable from https://web.stanford.edu/group/cslipublications/cslipublications/Online/doets-basic-model-theory....
- 53
0
votes
0
answers
35
views
Show $I\Vdash_{\Sigma} φ$ iff $I\Vdash_{\Sigma} \forall x φ$.
Let $\Sigma$ be a signature (decidable, with equality) and $I$ an interpretation structure over said signature. Let $φ$ be a formula. Show $I\Vdash_{\Sigma} φ$ iff $I\Vdash_{\Sigma} \forall x φ$.
...
- 363
0
votes
1
answer
40
views
what does p in "3-CNF-SAT ≤p SUBSET-SUMS" mean?
I come across this notation
from book "Introduction to Algorithm, CLRS", page 1097, but have no idea why p is subscript
Another source: https://www.youtube.com/watch?v=i8Kt9IBZ8FU
- 123
-1
votes
1
answer
316
views
Checking tautology
Given a Boolean formula $\phi$ in CNF form, I'll check whether there exists a clause that can be falsified i.e. check for literals of the form $x \vee \neg x$. If there are not any such literals in a ...
0
votes
1
answer
247
views
Are two formulae $\phi = p, \psi = \neg p$ equisatisfiable?
Two formulae $\phi$ and $\psi$ are equisatisfiable if both of them are satisfiable or none of them is satisfiable. And they can have their own independent truth assignments $\tau_{1}$ and $\tau_{2}$ ...
- 35
1
vote
0
answers
190
views
Is (3,3)-NAE-SAT NP-complete?
In this question I assume the following: in either $(i,j)$-SAT or $(i,j)$-NAE-SAT, every clause has exactly $i$ literals, and a given variable appears at most $j$ times in the entire formula. NAE ...
- 79
5
votes
1
answer
185
views
prove or disprove: every non satisfiable set of WFF has a non satisfiable sub set such every proper subset of it is satisfiable
Let $\Gamma$ be a non-satisfiable set of well-formed formulas (wff).
prove or disprove:
$\Gamma$ has a non-satisfiable subset $\Delta\subseteq\Gamma$ such that for every $\phi\subsetneq\Delta$ is ...
user846115
2
votes
1
answer
537
views
If the length plus the width of rectangle ABCR is 8, then find perimeter of circle given rectangle is in a circle
In the figure, arc SBT is one quarter of a circle with center R and radius $6$. If the length plus the width of rectangle ABCR is $8$, then find the perimeter of the shaded region.
Background: This is ...
user876009
0
votes
0
answers
32
views
Systems of linear homogenous inequalities: getting started
I have a number of questions of varying difficulties related to satisfying largish (as large as possible) systems of linear inequalities. I gather these aren't easy, so I'd be happy to get numerical ...
- 1,609
0
votes
1
answer
44
views
if for every finite statement set is satisfiable by 2 then any statement set is satisfiable by 2
Let S be a statement set of first order logic.
We say that it is satisfiable by 2 if one can split to 2 the set, so each set is satisfiable .
Prove or disprove, if every finite is satisfiable by 2, ...
- 129