# 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
Filter by
Sorted by
Tagged with
16 views

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-... -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 ... 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 ... 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 ... 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. ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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}... 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 ... 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 ... 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 ... 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, ... 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,... 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 ... 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) ∧ ∀... 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 ... 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. ... 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 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 ... 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]\... 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 ... 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 (... 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 ... 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}... 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 ... 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-...
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 ...
243 views

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 φ$. ...
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
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 ...
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}$ ...
1 vote
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 ...
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 ... 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 ... 