All Questions
Tagged with propositional-logic satisfiability
37 questions
2
votes
0
answers
42
views
Satisfiability of a boolean formula with two occurrences of each variable with a special ordering
I am interested in the complexity of a special case of the boolean satisfiability problem:
We are given a boolean formula, consisting only of the logical operators $\land$ and $\lor$ (that can be ...
- 161
0
votes
0
answers
24
views
Finding a common variable value among all SAT solutions
Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
2
votes
1
answer
224
views
Tseitin formula on 2-connected graph
How can we prove that for $\\\\$ every $\\\\$ 2-connected graph G with an odd number of vertices, the unsatisfiable Tseitin formula for it is minimally unsatisfiable, that is, if we remove even a ...
user167124
0
votes
1
answer
140
views
Resolution on weakening rule by derived clause
How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule:
$\frac{C}
{C \vee D}$
(A clause $C$ is implied by $F$ if for ...
user150715
2
votes
0
answers
25
views
SAT for clauses of the form "At most m out of n are false"
Recall some terminology: Let $\mathsf P$ be a finite set of propositional atoms, and let $\Phi$ be a proposition over $P$ that is generated from $\top$, $\bot$, $\neg$, $\wedge$, and $\vee$. Then:
A ...
- 171
0
votes
1
answer
34
views
How to get the formal model using propositional logic
Input
There are three chairs (1,2,3) in the same row.
We need to find a seat for three guests (a,b,c).
Constraints
The first guest does not want to be seated next to the third one (neither left nor ...
0
votes
1
answer
95
views
Logical Consequence - Equivalent Assertions
I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
- 9
1
vote
1
answer
84
views
Simple Skolemization Question
Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
3
votes
1
answer
84
views
Stalmarck's method: x ≡ x → z, does z have to be true?
I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that:
y $\to$ z $\equiv$ x
where x, y and z are booleans which ...
- 53
2
votes
3
answers
2k
views
Why is SAT based on the CNF?
I have been reading up on Boolean logic and, specifically, the Boolean satisfiability problem. I have seen several people mention that the expression must be converted to conjunctive normal form (CNF) ...
- 133
4
votes
1
answer
50
views
Is there a $L$-complete variant of SAT?
Many complete problem of different class of complexity has SAT variant. Like 3-SAT or $k$-SAT is $NP$-complete, Horn-SAT is $P$-complete, 2-SAT is $NL$-complete, and so on. So I was wondering if there ...
- 43
1
vote
1
answer
100
views
Incomplete definition of function- first order logic
Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations.
Let $\Sigma_2=\{c',g^2,R_1'^1,...,R_k'^1\}$ where $c'$ is constant, $g$ is ...
- 109
2
votes
1
answer
1k
views
Is it generally possible to convert CNF to Horn clauses?
My intuition is that it is not generally possible, but I cannot think of a proof.
- 379
-1
votes
1
answer
106
views
Equivalence of Horn formulas tractable?
Assume I have two Horn formulas $\phi_1, \phi_2$. Horn formulas are CNF formulas so that each clause has at most one unnegated literal. For example:
$x_1 \wedge (\neg x_1 \vee \neg x_2 \vee x_3 )\...
D.W.♦
- 166k
2
votes
2
answers
149
views
Equivalence of Krom formulas tractable?
Assume I have two Krom formulas $\psi_1, \psi_2$. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, $\...
- 165
1
vote
1
answer
1k
views
Is Monotone 3-SAT with exactly 3 distinct variables untractable?
I have given the following SAT variation:
Given a formula F in CNF where each clause C has exactly 3 distinct literals and for each C in F either all literals are positive or all literals are negated....
- 165
2
votes
1
answer
72
views
Programming in Propositional Logic article notation question
I was reading this article about propositional logic and transforming problems to SAT. The author often uses the following notation (taken from Dominating set section):
I don't understand what $[v,i]$...
3
votes
1
answer
592
views
Definition of 2-CNF (a.k.a Krom) formula
In my lecturer's notes, the following definition for a 2-CNF wff is given:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals.
However, there is ...
2
votes
1
answer
163
views
Significance of quantifier ordering in quantified boolean formulas (kQBF vs. QBF)
I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e
..." ...
- 123
0
votes
2
answers
495
views
Does the naive conversion of a Boolean Formula to CNF have a polynomial or exponential complexity?
I am reading the naive conversion to CNF, this procedure is explaining in this book book, but I have not found a conplexity analysis of this algorithm:
elimination of equivalence
Elimination of ...
4
votes
0
answers
74
views
Is there a correspondence of steps between DPLL and sequent-calculus?
Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid?
And given ...
- 273
2
votes
1
answer
50
views
Preserving a propositional formula
I know I must be getting stuck on notation. However, I'm having trouble following the logic in Example 1.2 in https://arxiv.org/pdf/cs/0611018.pdf. They define what preserving a propositional ...
3
votes
1
answer
112
views
Are there any techniques for checking whether a clause is subsumed by another clause when adding it to a cnf formula?
When doing variable elimination on a formula in cnf form, there is created a lot of new clauses. Is there any efficient way to check if these are subsumed by other, already existing clauses?
- 57
1
vote
1
answer
138
views
Does exist NP language that is Cook Levin deterministic reducible to xor satisfiability in polynomial time?
We say that the language $L$ is Cook Levin deterministic reducible to xor satisfiability in polynomial time if and only if for each word $w\in\Sigma^*:w\in L\iff f(w)\in XORSAT$ where $\Sigma=\{0,1\}$ ...
user82913
0
votes
1
answer
282
views
Is this possible to solve satisfiability by using Quine McCluskey algorithm to simplify the whole given boolean formula by simplifying subformulas?
In this question
Farewell Stack Exchange suggested to use karnaugh maps to solve the satisfiability problem by simplifying the entire/whole boolean formula by simplifying subformulas until you have ...
user82913
1
vote
1
answer
263
views
How to adapt DPLL to solve HORNSAT?
This question wask asked in a homework of Computer Theory in Rome, Italy.
How to simplify the DPLL algorithm in order to solve HORNSAT?
My Approach:
I know that an Horn clause is an OR of ...
- 187
1
vote
1
answer
1k
views
Is this possible to solve boolean satisfiablility by using karnaugh maps to simplify the whole given boolean formula by simplifying subformulas?
Building karnaugh map for the whole given boolean formula always costs Θ(2n) both time and space complexities, where $n$ is the number of boolean variables in the given boolean formula.
It is ...
1
vote
1
answer
1k
views
What is the complexity of determining whether or not conjunction of positive CNF and negative CNF is satisfiable?
Definitions:
positive CNF is a conjunctive normal form formula, where all literals are positive, i.e. the unary connective ¬ does not exist in the formula.
negative CNF is a conjunctive normal ...
0
votes
1
answer
473
views
Proving unsatisfiability of a propositional formula
I have a propositional formula $F$ and an assignment of truth variables $A$. The assignment $A$ assigns a truth value to each variable in $F$ and then it can be evaluated.
I have a function which for ...
- 427
1
vote
1
answer
705
views
Is this possible to solve 4SAT in polynomial time? [closed]
I know and admit that this is long, but please read it slow and understand everything.
I think that this is one of the most interesting questions asked in computer science ever.
I don't expect for ...
5
votes
3
answers
5k
views
Find hamilton cycle in a directed graph reduced to sat problem
I need to find a Hamiltonian cycle in a directed graph using propositional logic, and to solve it by sat solver. So after I couldn't find a working solution, I found a paper that describes how to ...
- 53
2
votes
1
answer
136
views
Non-deterministic algorithms and Tautologies
I am studying the lecture The Complexity of Propositional Proofs. Here there is a definition together with a discussion (page 3). I don't understand
that discussion.
Let $F$ denote the set of ...
- 503
2
votes
1
answer
115
views
Complexity of a SAT related problem
Given a set of (propositional) formulae $\Phi$, two formulae $\phi$ and $\xi$, determine whether there exists $\Psi\subseteq \Phi$ such that $\Psi\models \phi$ and $\Psi\not\models \xi$.
Question: ...
- 21
1
vote
0
answers
142
views
Efficiently decidable logics
So propositional logic (PL) is efficiently (in P) decidable because I can convert formulas to an equisatisifiable CNF-formula, negate and convert (efficiently, by De Morgans laws) to DNF. I can then ...
- 3,800
3
votes
2
answers
778
views
Getting a variable assignment of a Tseitin transformed formula
Let $\phi$ be a Boolean formula and $\mathrm{Tseitin}(\phi)$ the corresponding Tseitin transformed equisatifiable formula.
It is well-known that one can get a variable assignment for $\phi$ by ...
- 259
1
vote
1
answer
101
views
Satisfiabilty 2-sat
Im trying to work out whether the following clause is satisfiable:
{x, y},{x,¬y},{¬x, y},{¬x,¬y},{x, z},{x,¬z},{y, z},{y,¬z}
My basic understanding is to work ...
- 469
2
votes
4
answers
4k
views
Resolution and what it means to derive the empty set
When using resolution, if the empty set {Ø} is derived from a formula like {¬x,¬y} {x,y}, does that mean the formula is unsatisfiable?
If this is the case, why is ...
- 469