# 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.

332 questions
Filter by
Sorted by
Tagged with
21 views

### Satisfiability of certain class of 2-CNF formulae

A propositional formula in conjunctive normal form (from now on abbreviated CNF) is said to be in standard form if there are no pure literals, no duplicated clauses, and no possible resolutions in ...
18 views

### Guess the number in the box - which complexity class does this belong in?

I'm trying to improve my understanding of complexity classes by reading the complexity zoo here, https://complexityzoo.net/Complexity_Zoo, and a number of other resources. I'm having an argument with ...
• 1
1 vote
109 views

126 views

### Application of blocked clauses

I read from this question, I have not understood $G$ satisfiable $\implies F$ satisfiable section. In this section case3 is $D$ contains $\bar\ell$. And author said in the last line "blocked ...
303 views

### Proving Pigeonhole Principle is Unsatisfiable

Consider the resolution rule, that is, I can add a resolvent of any two clauses to the formula. My question is: From using only this above rule how to show that the pigeon-hole formula for 3 pigeons ...
185 views

• 7,243
40 views

### how to construct BDD from huge logic expression?

I have a multi-valued discrete logic expression looks like this: 0.03*A+0.005*B+0.4*C+... + 0.006*N >= 0 It has 14 variables (from A to N), each variable has ...
86 views

### Show that the direct product of structures satisfies a Horn sentence

This is exercise 3.4.16 from Mathematical Logic by Ebbinghaus. Formulas which are derivable in the following calculus are called Horn formulas: Horn formulas without free variables are called Horn ...
1 vote
60 views

### Solving an SAT problem with objective

I have 8192 bits, denoted $b_0, b_1, ..., b_{8191}$. The bits are subject to some XOR constraints (e.g. $b_0 \oplus b_3 \oplus b_{42} \oplus \cdots \oplus b_{8191} = 1$). The objective function to be ...
• 854
60 views

### What is the Tseitin transformation of a single literal?

The wikipedia page for Tseitin transformation includes a nice example of the transform itself. In the example, it is implied that there is no need to create a fresh variable for a single literal (that ...
• 521
1 vote
87 views

### Show that $(\forall v_1)\neg(\forall v_2)\neg (v_1 = v_2+v_2)$ is false in $\mathfrak{N}$.

I am self studying 'A Friendly Introduction to Mathematical Logic' by Christopher C. Leary and am struggling to follow Example 1.7.10 which I have simplified as follows: Let $\mathcal{L}$ be the ...
62 views

168 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 ...