Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

0
votes
1answer
30 views

Use Horn formula to prove that it is possible to produce carbonic acid

I don't know how to translate this problem to mathematical logic language. How am I supposed to came up with a Horn formula from this? I should easily be able to test it's satisfiability after that, ...
1
vote
2answers
50 views

FOL - If two models agree on every sentence are they isomorphic?

Let $M,N$ be two models. If for every sentence $\varphi$, $M\models \varphi \iff N\models \varphi$ then they are isomorphic. My intuition is that that the claim above is incorrect. While the other ...
0
votes
1answer
49 views

If F satisfiable then ¬F is unsatisfiable.

If F satisfiable then ¬F is unsatisfiable. I know this is false and to show this I need to show a contradiction, this is my attempted answer, any ideas where I'm going wrong, this is revision for an ...
0
votes
0answers
9 views

How to find values for these variables?

I have four unknowns and one equation. Is there a way to assign non-trivial values to them? The variables are: $$q_0, q_1 \in [0, 1] \\ e_0, e_1 \in [{z \in \mathcal{C} : \lvert z \rvert \le 1}]$$ ...
1
vote
1answer
37 views

$\Gamma_1 \cup \Gamma_2$ is not satisfiable iff there exists $\alpha \in WFF$ such that $\Gamma_1 \vdash \alpha$ and $\Gamma_2 \vdash \lnot \alpha$

Let $\Gamma_1,\Gamma_2 \subseteq WFF.\;$ Prove: $\Gamma_1 \cup \Gamma_2$ is not satisfiable if and only if there exists $\alpha \in WFF$ such that $\Gamma_1 \vdash_{HPC} \alpha$ and $\Gamma_2 \vdash_{...
0
votes
1answer
15 views

satisfying boolean n variable DNF formula

I have an n variable boolean DNF formula and an input set,z consisting of n-tuples. Each tuple consists of truth/false assignment to n variable. the number of tuples in Z is not fixed, obviously <= ...
1
vote
1answer
38 views

Is there a standard quantifier notation for an exact number of true values?

When working with SAT Solvers, I need to write quantifiers that give the total number of true values. The usual quantitiers $\forall$ and $\exists$ do not suffice. Is there a standard notation for ...
0
votes
0answers
14 views

How would I reduce the Minimum Vertex Cover problem to a Weighted MAX SAT problem?

I am currently trying to solve the Minimum Vertex Cover problem via a Weighted MAX SAT solver, but I am stuck with the model. The transformation to a simple SAT is straightforward since every node can ...
1
vote
1answer
34 views

how to convert linear equation to cnf

I'm working on reduction from binary puzzle problem into sat. one of the game's rule is that in each row/column numbers of 1s equals to numbers of 0. I found a solution but it's exponential. Therefore,...
1
vote
0answers
21 views

What is the fastest, free Weighted SAT solver?

I want to solve the minimum vertex cover problem by solving and equivalent SAT instance. I tried several solvers, but I didn't find any solver which does weighted SAT. Do you know of any free SAT ...
1
vote
1answer
52 views

Eigenvalues and BIBO stability

Could someone please explain to me the relationship between eigenvalues of a system matrix A and BIBO stability? I've studied control engineering, and for example in modern control, we say that a ...
1
vote
3answers
63 views

Compactness Theorem for Propositional Logic

Here is the compactness theorem: If every finite subset of $\Phi$ is satisfiable, then $\Phi$ is satisfiable. Is the contrapositive the following? If $\Phi$ is unsatisfiable (tautologically ...
1
vote
2answers
70 views

How to use resolution to prove a sentence is unsatisfiable?

I need to use resolution to prove this sentence is unsatisfiable. $(p\lor q \lor \neg r) \land ((\neg r \lor q \lor p) \to((r \lor q) \land \neg q \land \neg p))$. My clausal form is this. $\{{ p, q, \...
0
votes
1answer
24 views

Validity and Satisfiability problem.

Formula F is equivalent to formula G iff A) F IFF G is valid B) F IFF NOT(G) is not valid C) F XOR G satisfiable D) F XOR G is not satisfiable I have been told solution D is correct. How is this ...
1
vote
0answers
24 views

Number of X3SAT Instances

Exactly 1 in 3SAT (X3SAT) is a variation of the boolean satisfiability problem. Given a 3CNF instance is there a satisfying assignment where exactly one literal in each clause is true? X3SAT is known ...
0
votes
1answer
32 views

Can any 1st-order proof be expressed with an SMT?

Is it possible to rephrase every proof which uses first-order logic into a proof which uses satisfiability modulo theories? In other words, can a program which automatically solves SMT questions solve ...
9
votes
3answers
567 views

Why does Skolemming not preserve validity?

I'm wondering what exactly is meant when people say "Skolemization preserves satisfiability but not validity". I'm having trouble wrapping my brain around it because I think of Skolemization, when ...
0
votes
0answers
65 views

A Language in CNF with distinct variables per clause and each variable appears in at most three literals is in P

Let A be a language defined thus A = {φ | φ is in CNF, with three literals, comprising distinct variables, per clause; and each variable appears in at most three literals; and φ is satisfiable} . ...
0
votes
1answer
33 views

NP Completeness of a Graph Problem, Proof Required

I have a graph problem that I would like to prove NP-completeness. It is outlined below: A graph problem compromising of two graphs, say $G_1(V_1,E_1)$ and $G_2(V_2,E_2)$ such that $V_i$ and $E_i$ ...
1
vote
1answer
51 views

Does this solve boolean satisfiability problem in polynomial time?

CNF can be easily converted into a formula that uses only AND and NOT operations, using the fact that ...
0
votes
0answers
118 views

how to convert SAT to 3SAt

My teacher showed these steps when converting SAT to 3SAT (he was working with an example). He said to construct a formula F1 ...
0
votes
0answers
37 views

Computational Treatment: Relational Isomorphism Problem

We consider relational systems $(X_1,Y_1,R_1)$ and $(X_2,Y_2,R_2)$ with $R_i\subseteq X_i\times Y_i$. An isomorphism is a pair of bijective maps $(\alpha,\beta)$, with $\alpha: X_1\rightarrow X_2$ and ...
2
votes
1answer
61 views

How to determine a FOL structure which satisfies a given formula

I have the task: Consider the formula $\forall x (Q(x,b) \to Q(b,x))$ where $Q$ is a binary predicate symbol and $b$ is an individual constant. State i) one non-satisfying, and ii) one ...
0
votes
0answers
56 views

Has the satisfiability of the following horn expressions correctly been determined? [verification]

I have the following task "Check the following expressions with the horn satisfiability algorithm, and, if necessary, provide an assignment which fulfills satisfiability." $((\neg q \lor \neg p) \...
0
votes
0answers
20 views

USAT, Arora Barak's book

Here on the page 354 Arora and Barak write below the shaded area "but in fact $f(\phi)$ $\notin SAT$" and not "but in fact $f(\phi) \in SAT$" While in the last line of the shaded area they write $...
1
vote
0answers
20 views

Ratio between clauses and variables

How is the ratio between the number of clauses to the number of variables in a HORNSAT sentence correlated with its probability to be satisfied? My intuition tells me that the more variables I have, ...
2
votes
0answers
72 views

Finitely satisfiable sets of formulas

The following problem is from the book "A Beginner's Guide to Mathematical Logic" by Raymond M. Smullyan in the context of preparing a (second) proof of the compactness theorem for propositional logic ...
0
votes
1answer
59 views

Does a 3SAT instance need to have exactly three terms in each clause?

For example, is (x \/ ~y ) /\ (~x \/ y \/ ~z) valid? I have read conflicting descriptions of 3SAT where some say you must have exactly 3 terms in each clause, ...
1
vote
2answers
107 views

$\phi$ is a $m$-clause CNF formula. Prove that if $m< 8$, then there is at least 1 satisfying assignment for $\phi$.

$\phi$ is a 3SAT CNF formula. All variables in each clause of $\phi$ are distinct. The expected number of satisfied clauses under the uniform random assignment is given as $\frac{7m}{8}$. A satisfying ...
0
votes
2answers
97 views

How to prove that adding elements to a set does not affect its satisfiability?

Prove that adding a unit clause on a new atom to a set of clauses and adding its complement to clauses in the set preserves satisfiability. I don't how to do it. Could someone give me hints to prove ...
1
vote
1answer
204 views

How exactly are consistency and satisfiability related in first order logic?

A set $\Gamma$ is consistent if there is $\psi$ such that $\Gamma \not\vdash \psi$. A set $\Gamma$ is satisfiable if there is a model such that $\Gamma \vDash \psi$ for any $\psi \in \Gamma$. ...
3
votes
2answers
194 views

A formula is satisfiable under $I \iff |I|=1$?

Let $A(x_1, . . . , x_n)$ be a formula with no quantifiers and no function symbols. Prove that $∀x_1 · · · ∀x_nA(x_1, . . . , x_n)$ is satisfiable if and only if it is satisfiable in an ...
1
vote
0answers
60 views

Rainer Schuler's algorithm of CNF SAT problem

I'm reading through this publication trying to understand the algorithm and what exactly did Schuler achieve compared to Cook's theorem. Can someone please explain me how this algorithm works in ...
4
votes
1answer
154 views

Why doesn't implication graph work for 3SAT as it does for 2SAT?

I am trying to understand why it is not possible to use implication graphs, that work to solve $2SAT$, to solve $3SAT$ or $kSAT$ in general. Intuitively I think its because implication extends from ...
0
votes
1answer
69 views

Induction on formulas for substitution

Let's say that $φ$ is a formula, $M$ is a structure, $t'$ is a term, $s$ is a variable assignment, and $s'$ is an $x$-variant of $s$ such that $s′(x)=Val^M_s(t')$. I need to use induction on ...
1
vote
0answers
45 views

Integer Programming (non $0-1$) Reduction to show $NP$ Completeness

I'm having trouble coming up with a reduction for the integer programming problem when the variables aren't constrained to $0$ or $1$. For the case where the variables are constrained to $0$ or $1$, ...
1
vote
1answer
117 views

Divide and conquer SAT Solver

Are there any SAT solver algorithms which break up a 3SAT sequence of $m$ clauses into $n$ parts, solve these $n$ parts in parallel and then combine the solutions from each part into a final solution ...
1
vote
1answer
96 views

First Order Logic - Logical Consequence and Paradox

When we use the Resolution Principle we try to deduce a logical consequences from 2 clauses. The set of clauses is unsatisfable , if we get a empty clause. What i dont understand is : in practice, ...
1
vote
2answers
141 views

First Order Logic - unsatisfiable set of formulas

I know what is an unsatisfiable set of formulas in first order logic and I'm studying how to prove the unsatisfiability. What I don't understand, I'm sorry a think as an engineer, is what get in ...
0
votes
1answer
15 views

How to I correctly specify the following set of sets of edges of a graph

I have a directed, edge-labled, loop-allowed, double-edge-disallowed (with different label allowed, with same disallowed that is) Graph $G$ with Vertices $v\in V_G$ and Edges $e\in E_G$. Each edge ...
0
votes
2answers
75 views

Is $\forall_x\forall_y\forall_z\Big(P(x,x)\wedge(P(x,z)\implies\big(P(x,y)\vee P(y,z)\big)\Big)\implies\exists_x\forall_y P(x,y)$ tautology?

Is formula $$ \forall_x\forall_y\forall_z\Big(P(x,x)\wedge(P(x,z)\implies\big(P(x,y)\vee P(y,z)\big)\Big)\implies\exists_x\forall_y P(x,y) $$ a tautology? What's method to check this? Do I need to ...
0
votes
0answers
38 views

Is it possible to solve the FACT (integer factorization) problem in polynomial time if we know the polynomial Subset Sum algorithm?

Is it possible to solve the FACT (integer factorization) problem in polynomial time if we know the polynomial Subset Sum algorithm? We assume that we know the algorithm solving the problem of Subset ...
0
votes
1answer
179 views

Reduction 3SAT to Subset Sum

I have a problem. We have a document (page 4 - table) or this book (page 314 in PDF / page 293 in book numeration - table). The question is: How should we read the decimal values in this table? From ...
0
votes
0answers
20 views

How do I derive the formula for the expected number of models of a set of $L$ Boolean clauses with $N$ variables?

Reading the paper "The SAT Phase Transition" by Ian Gent and Toby Walsh, I found something that confused me. On page 5, in Section 3, the authors say that, if $\phi(k)$ is the probability that a ...
2
votes
1answer
31 views

validity reduction between FOL fragments

Let $\Sigma_1=\langle R^2,P^1,=\rangle$ a dictionary with $R$ a binary relation, $P$ an unary relation and equality. Let $\Sigma_2=\langle c,f^1,=\rangle$ a dictionary with $c$ a constant, $f$ an ...
2
votes
1answer
256 views

How to prove that 3-CNF is satisfiable using Hall's marriage theorem?

Given a 3-CNF formula where each variable from variables $x_1,...,x_n$ appears exactly 3 times in different clauses $c_1,...,c_m$, and each clause contains exactly 3 different variables, prove that ...
1
vote
0answers
56 views

Unsatisfiable $X_3SAT$ Instances

Exactly $1$-in-$3$ SAT ($X_3SAT$) is a variant of the Boolean satisfiability problem. Given a set of clauses, each clause having three literals, is there a set of literals such that each clause ...
0
votes
2answers
59 views

if p v r is satisfiable then p is satisfiable

When checking if a propositional logic is true or not, do you need to consider all possible models of it? For example in this question: if p v r is satisfiable then p is satisfiable If ...
1
vote
1answer
57 views

Randomized algorithm to satisfy conjunctive clauses

There are $m$ clauses containing a conjunction of 3 variables out of $n$ Boolean variables. (they are of the form $x_i$ $\wedge$ $x_j$ $\wedge$ $x_k$, where each $x_{i,j,k}$ is a variable or it's ...
0
votes
2answers
49 views

∃xA(x) ∧ ∃x¬A(x) is this formula satisfiable ?

I am little confused regarding satisfiabilty problems. can someone help me to understand whether ∃xA(x) ∧ ∃x¬A(x) is satisfiable or not ? and if yes what is the minimum number of elements in each ...