Stack Exchange Network

Stack Exchange network consists of 175 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
0answers
55 views

Is there an instance 3-SAT on which this algorithm fails?

I'm not sure on how to express that in a very formal and absolutly correct way so I hope it is still understandable. I have found this algorithm and been struggling for a while proving it does or ...
1
vote
1answer
33 views

Using the reduction of 3-SAT to 3-COLOR, explain why complexity proofs by reduction work.

I'm reading about the proof that 3-COLOR is in NP-Hard, by reduction of 3-SAT to 3-COLOR (as listed here for example: http://cs.bme.hu/thalg/3sat-to-3col.pdf). And here's a passage from Wikipedia, ...
1
vote
2answers
14 views

SAT for a formula using Tableaux Propositional Logic (precedence of operators)

My doubt is in check if the following formula $\phi$ is SAT or not using the Tableaux Method. Let me write formula: $\phi = \neg \left ( p \vee q \supset \left ( \left ( \neg p \wedge q \right ) \...
2
votes
1answer
60 views

Is it consistent with NBG that there are two different satisfaction classes that satisfy the Tarski conditions?

So, NBG can not prove that first order set theory has a satisfication class. However, it is consistent with NBG that such a class exists. My question is if it is consistent with NBG that two such ...
1
vote
0answers
9 views

Faster boolean expression satisfaction

Few months ago I started to code message filtering for email. The filters are basically set of boolean operators, for example OR(Has(a), NOT(OR(Has(b),Has(c))), AND(Has(e), Has(f)))..., that decide ...
3
votes
1answer
19 views

convert biconditional to pseudo-boolean (inequality / equation) constraints

I am working with pseudo-Boolean and I want to convert the bi-conditional $(a \land b) \iff c$ to inequality or equation. my attempt was. First, convert the bi-conditional to two implies $$((a \...
1
vote
1answer
37 views

Example of a complete and consistent set of formulas in propositional logic

So, I am aware that every set which is inconsistent is complete (every formula can be derived from it) and that a set is consistent if and only if it is satisfiable. But what is an example of ...
2
votes
1answer
39 views

What's the meaning of “$F \models \bot$” in propositional logic?

For example, in the demonstration that $F \vDash \bot \iff \forall G.F \vDash G $ how do I use the $F \vDash \bot$ hypothesis? Thanks in advance.
2
votes
1answer
21 views

SAT with DPLL algorithm: Why is this not correct?

I've got an exam soon and have problems understanding a specific error when performing the DPLL algorithm by hand: We use 2 additional rules for the algorithm: One literal rule (OLR) and pure-literal ...
1
vote
1answer
23 views

Divisibility represented by Boolean logic

Some context: I was thinking about the feasibility of using SAT solvers to prove primality, especially of Mersenne primes, by showing that there exists no Boolean sequence $d_1,d_2, ..., d_{b'}$ that ...
2
votes
1answer
50 views

Reduction from 3-SAT to MAX 2SAT

For some time I've been trying to understand reduction of 3-SAT to MAX 2-SAT. I reviewed most of most popular books about computational complexity (Thomas Cormen, Papadimitriou) but I can't find an ...
0
votes
0answers
37 views

What could be the formal mathematical meaning of “onto over?”

I found an author who likes to use the phrase "$\underline{\textbf{onto over}}$" For example, the textbook author might write: The set $X$ projected $\underline{\textbf{onto over}}$." the variable ...
0
votes
0answers
33 views

Unsatisfiable Union but parts can be satisfied by P and not P

Suppose that G1 and G2 are theories and that G1 Union G2 is unsatisfiable. Prove that there is a sentence P s.t. every model of G1 satisfies P and every model of G2 satisfies not P. I do not entirely ...
1
vote
2answers
44 views

First-order formulas with exponentially large models

The separated fragment of First-Order Logic (FOL) is the sublanguage of FOL in which no atomic sub-formula $A(\ldots,x,\ldots,y,\ldots)$ is such that $x$ is bound by and existential quantifier and $y$ ...
0
votes
0answers
29 views

3-SAT with few variables

I am wondering what is the complexity status of 3-SAT when the number of variables is small compare to the number of clauses. Let n be the number of variables plus the number of clauses. It is clear ...
0
votes
1answer
32 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
68 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 ...
1
vote
1answer
67 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
40 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
21 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
43 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
16 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
42 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
27 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
2answers
84 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
106 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
189 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
34 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
26 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
578 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
67 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
92 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
138 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
79 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
62 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
24 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
99 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
84 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
115 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
98 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
247 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
202 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
62 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
168 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
77 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 ...