Skip to main content

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.

Filter by
Sorted by
Tagged with
0 votes
0 answers
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 ...
John Baxenden's user avatar
0 votes
0 answers
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 ...
3mar's user avatar
  • 1
1 vote
1 answer
109 views

How to use resolution in this formula with XOR? [closed]

Transform the set of causes of the given formula are below: $\overline{x}\lor y.....(1)$ $\overline{y}\lor x.....(2)$ $\overline{z}\lor w.....(3)$ $\overline{w}\lor z.....(4)$ $\overline{s}\lor \...
user avatar
0 votes
1 answer
52 views

Resolution Exponential Memory Blowup

I'm looking at the Davis-Putnam algorithm. I don't understand how resolution results in an exponential blowup in the size of the formula, since it seems that after each step, the size is reduced. $(...
David Cheung's user avatar
0 votes
1 answer
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 ...
user avatar
0 votes
2 answers
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 ...
user avatar
0 votes
1 answer
185 views

How to prove that the following simplification rule on Davis–Putnam function is satisfiability-equivalent?

Denote $F\stackrel{\text{SAT}}{\equiv}H$ if $F \in SAT {\iff} H \in SAT$. A transformation of formulas $S(·)$ is called satisfiability-equivalent if $\forall{F}\space F\stackrel{\text{SAT}}{\equiv}S(F)...
user avatar
0 votes
1 answer
55 views

Does finding feasible solution to set cover problem is as hard as SAT problem?

I have a weird feeling that finding a single feasible solution to the set cover problem is as hard as SAT problem. I think that this might be wrong but I am not sure why. To illustrate my thinking, ...
Tuong Nguyen Minh's user avatar
2 votes
1 answer
361 views

How to prove that the following simplification rule is satisfiability-equivalent?

Denote $F\overset{\text{SAT}}{\equiv}G$ if $F \in SAT {\iff} G \in SAT$. A transformation of formulas $S(·)$ is called satisfiability-equivalent if $\forall{F}\space F\overset{\text{SAT}}{\equiv}S(F)$....
S. M.'s user avatar
  • 1
2 votes
0 answers
52 views

Positive boolean satisfiability problem : finding minimal solutions.

Consider, over a finite set of boolean variables X, a Boolean system in CNF (conjunctive normal form) whose clauses only contain non-negated literals. For every assignment of the variables which ...
Christopher-Lloyd Simon's user avatar
0 votes
1 answer
26 views

Looking for Efficient Encoding Permutations with Boolean Variables [closed]

I'm exploring the use of SAT solvers to find a permutation of the numbers 1, 2, and 3, subject to specific constraints. Initially, I considered employing nine variables: $x_{1,1}, x_{1,2}, \dots, x_{3,...
LeafGlowPath's user avatar
  • 7,243
0 votes
0 answers
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 ...
QianruZhou's user avatar
2 votes
1 answer
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 ...
iwjueph94rgytbhr's user avatar
1 vote
1 answer
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 ...
nalzok's user avatar
  • 854
0 votes
0 answers
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 ...
ampersander's user avatar
1 vote
1 answer
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 ...
user neme's user avatar
0 votes
1 answer
62 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-...
Jova's user avatar
  • 433
1 vote
0 answers
42 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 ...
Anwarul Azim's user avatar
1 vote
1 answer
131 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 ...
WillG's user avatar
  • 6,620
0 votes
0 answers
37 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 ...
Tilo RC's user avatar
  • 11
0 votes
1 answer
64 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. ...
happyle's user avatar
  • 183
3 votes
1 answer
156 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 ...
HighAsAKiteOnMath's user avatar
3 votes
0 answers
62 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 ...
Tejas's user avatar
  • 141
2 votes
1 answer
117 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 ...
effezeta's user avatar
  • 455
4 votes
1 answer
100 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 ...
k-ecker's user avatar
  • 41
1 vote
0 answers
16 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 ...
Theo Deep's user avatar
  • 247
1 vote
1 answer
42 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 ...
Emil Sinclair's user avatar
0 votes
1 answer
51 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 ...
Turkhan Badalov's user avatar
0 votes
2 answers
82 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}...
Turkhan Badalov's user avatar
0 votes
1 answer
40 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: ...
young amogus's user avatar
0 votes
1 answer
58 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 ...
Alex Woolfe's user avatar
0 votes
0 answers
62 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 ...
Alex Woolfe's user avatar
0 votes
1 answer
62 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,...
Selena J's user avatar
  • 153
4 votes
0 answers
196 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 ...
mghandi's user avatar
  • 1,792
4 votes
1 answer
127 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) ∧ ∀...
Scorate's user avatar
  • 43
0 votes
0 answers
31 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 ...
P. Quinton's user avatar
  • 6,056
0 votes
0 answers
27 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) ...
Avijeet Ghosh's user avatar
1 vote
0 answers
29 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 ...
Stefania Dokker's user avatar
0 votes
1 answer
50 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. ...
juaninf's user avatar
  • 1,264
0 votes
1 answer
50 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 (...
Estaban's user avatar
1 vote
1 answer
129 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 ...
cozzie9806's user avatar
1 vote
1 answer
48 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]\...
Qcer's user avatar
  • 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 $...
Christof Tinnes's user avatar
0 votes
1 answer
217 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 ...
cozzie9806's user avatar
3 votes
1 answer
561 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 (...
Abhishek Ghosh's user avatar
0 votes
1 answer
73 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 ...
user avatar
2 votes
0 answers
58 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}...
user avatar
4 votes
1 answer
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 ...
user avatar
0 votes
1 answer
32 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-...
komorra's user avatar
  • 123
0 votes
2 answers
48 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 ...
knightgambit's user avatar

1
2 3 4 5
7