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
2
votes
0answers
32 views

How can I use a SAT solver to find a configuration that is not satisfiable?

For the following graph, I can easily setup clauses that use variables $E_{0,3}$, $E_{1,3}$, and $E_{2,3}$ for the 3 potential new edges, so that a SAT solver can find all the graphs that are 3-...
1
vote
1answer
36 views

n-Queens problem possible solutions by logical equivalences

I'm studying Discrete maths recently, mainly through MIT 6042J and Rosen's Discrete Math and its applications. In the later, I found the following problem I can't figure out how to proceed: The ...
0
votes
1answer
42 views

Solving 3-SAT with Linear Programming?

Suppose we have a set of indices $I = \{1, \dots, n\}$ and a corresponding set of boolean variables $\{X_1, \dots, X_n\}$. Suppose further that we have a 3-CNF expression with $m$ clauses, with ...
0
votes
0answers
13 views

which similar np hard problem can be used to reduce timetabling problem?

I have a set of courses and each courses have a set of classes. Each classes have a set of timings available with some penalty. I wanted to schedule each classes to any of the timings of its with a ...
3
votes
1answer
39 views

Proving that unary predicates theory has no $T$-complete formulas

As a follow up to my previous question, as suggested in the comments, I would like to know a way how to prove that the theory of infinitely many unary predicates, is axiomatized by the sentences $\...
1
vote
0answers
20 views

Is there a complexity class MAJ-QSAT?

Let $A$ be a propositional formula in $n$ variables. Then we can denote by $\sharp A$ the number of assignements that make $A$ true. $\sharp A$ can have a value in the range $0..2^n$. We can compute ...
4
votes
2answers
124 views

Prove that a wff built up only with $\lnot$ and $\leftrightarrow$ is a tautology iff $\lnot$ and each statement letter occur an even number of times.

First of all, I know how to prove this theorem below: A statement form that contains $\leftrightarrow$ as its only connectives is a tautology iff each statement letter occurs an even number of times....
6
votes
1answer
214 views

Is XOR-SAT + $2$-SAT in P?

I read in a paper a proof where you can reduce a $3$-SAT problem into $2$-SAT + HORN-SAT clauses. $2$-SAT + HORN-SAT is therefore, NP-complete. $2$-SAT, HORN-SAT, DUAL HORN-SAT, XOR-SAT are all in P. ...
2
votes
1answer
122 views

Can travelling salesman be translated into a SAT problem? [closed]

I read that all NP-complete problems can be translated into one another. I can't see how the travelling salesman problem which involves distances which are real numbers can be translated into a ...
3
votes
2answers
41 views

Is 3-SAT useful for anything practical?

If all NP-complete problems can be converted to 3-SAT problems I had an idea that would not solve the NP problem but might be a practical solution. What you could do is simply, make a huge table of 3-...
0
votes
0answers
27 views

Is approaching my problem as a SAT problem a good approach? Enormous number of clauses.

Let me first introduce the problem. I have prepared an illustrative picture. There is a blue box with $I$ inputs. Blue box contains $Y$ yellow boxes. Each yellow box contains $R$ red boxes. Each red ...
1
vote
0answers
26 views

Disjunctive normal form simplified of one solution problem

One thing I'm interested in knowing is: In general if there was a Boolean equation that you knew only one possible assignment of its variables would make it true. Then can it always be simplified ...
0
votes
1answer
48 views

Show that $\Phi \vDash \psi \Longleftrightarrow \Phi \cup \{\lnot \psi\} \ \text{is not satisfiable}$

The main algorithmic problems in logic (in my bachelors CS course) are: $0)$ evaluation problem "Auswertungsproblem", $1)$ equivalence problem, $2)$ logical consequence, $3)$ satisfiability ...
0
votes
0answers
27 views

Dominant set of a Graph - Convert to Conjunctive Normal Form

I am supposed to convert this problem to a Satisfiability Problem in Conjunctive Normal Form, but I have no idea how. The Problem: Determine, if there exists any dominant set for a Graph $G$ ...
0
votes
0answers
15 views

Construct satisfiable solution to a bunch of constraints

I have to determine a problem is feasible or not, but I am not sure how to categorize my problem. It's not LP, or other standard forms of feasibility problems I've encountered. The specific problem is ...
1
vote
0answers
16 views

Terminology for Linear Programs without Objective Functions

I have a linear program without an objective function. That is, I am looking for a feasible solution to a given set of linear constraints. Is there a specific term for such problems? Likewise, for ...
0
votes
1answer
63 views

How do you determine if a formula is satisfiable in Predicate Logic?

For example: $ (\forall x)(P(x) \rightarrow Q(x))$ Are you suppose to invent your own Interpretation (domain, and giving the meaning to the predicates), and make it satisfiable under that ...
0
votes
1answer
47 views

CNF formula for manipulating words

I am trying to create CNF formula for manipulation of a word. word is a sequence of letters from a $\Sigma$ alphabet. A word is encoded by variables like $x_{i,a}$ which means that the letter $a$ is ...
0
votes
1answer
27 views

CNF for modilisation of a word

Imagine that we are interested in problem of words. A word is a sequence of letters from a $\Sigma$ alphabet. For encoding a word in SAT we are using variable like $x_{i,a}$ which means that in ...
1
vote
1answer
83 views

Finding the logical consequence of a set of formulas $A$

I am trying to solve an exercise that gives me a set $A$ of formulas such that $A = \{ p, (r → q) → ¬p, (r ∨ p) → q, r\}$ and wants me to compute $Cn(A)$, knowing that in the textbook $Cn$ (...
1
vote
1answer
40 views

Converting a 4cnf clause into one with not all equal literals

Given a 3cnf clause $$(a \lor b \lor c)$$ we can construct an equivalent conjunction $$(a\lor b\lor d) \land (\lnot d \lor c \lor \bot)$$ such that the second clause has a valid truth assignment if ...
2
votes
1answer
57 views

resolution - satisfiability of formula (edit: renaming clause variables)

I need to determine whether the following formula is satisfiable, using binary resolution: $$\exists x \forall y \forall z ((P(y) \to Q(z)) \to (P(x) \to Q(x)))$$ I re-framed the problem to showing ...
0
votes
1answer
20 views

Is there an algorithm for reducing CNFs further

I have a boolean formula in conjunctive normal form (CNF): $(a\vee b \vee c) \wedge (a \vee b \vee \neg c) \wedge (x \vee y)$ I know that this can be simplified to: $(a\vee b)\wedge (x \vee y)$. a) Is ...
1
vote
1answer
88 views

How to obtain the empty clause from CNF?

I have the following formula $\mathcal{F} = A(c, y) \wedge A(c, z) \wedge \neg E(c, z) \wedge \neg A(z, c)$ from which I've derived the clauses $\{A(c, y)\},\{A(c, z)\},\left\{\neg E\left(c, z_{1}\...
2
votes
1answer
47 views

Boolean operator in Queen problem

In this paper, (page 28) I see the rule for there must be a queen in each row. My question is shouldn't it be: Xi1 & Xi2 &....XiN ...instead of: ...
6
votes
0answers
125 views

Bounds related to satisfiability problem

This question is regarding MAX E3SAT problem: Given a set of clauses with exactly three literals, find the maximum number of clauses that can be satisfied. The clauses are expressed as disjunctions of ...
5
votes
2answers
135 views

Analysis of Schöning's $k$-SAT algorithm

In his paper "A Probabilistic Algorithm for $k$-SAT and Constraint Satisfaction Problems", Schöning gives a randomized algorithm for $k$-SAT. The analysis conditions on the Hamming distance ...
0
votes
0answers
18 views

Is there an infinite or finite model or both that satisfy the following FO-formula?

Theres the following set of sentences: $\Phi$ := Ψ ∪ {∃x∃y x $\neq$ y, ∃x(ψ(x) ∧ ∀y(x $\neq$ y → ¬ψ(y)))} Whereas Ψ := {∀x∀y∀z(¬R(x, x) ∧ (x $\neq$ y → (R(x, y) ↔ ¬R(y, x))) ∧ (R(x, y) ∧ R(y, z) → R(x,...
1
vote
1answer
39 views

What is wrong with this definition of a truth predicate?

Tarski's theorem, interpreted in Peano Arithmetic, says there is no predicate $T$ such that $PA\vdash T(\phi)\leftrightarrow \phi$. However, we know that there are partial truth predicates for each $k&...
0
votes
1answer
32 views

First Order Logic : Satisfiability of an amount of Formulas

Let's take Σ that contains an amount of formulas A, B... We have that : Σ |= A exactly when Σ ∪ {¬A} unsatisfiable. Does this mean that if Σ and A both satisfiable are, then Σ ∪ {A} satisfiable ? =&...
0
votes
1answer
40 views

What is the dependency between the equivalence of consistence and satisfiability, and correctness and completeness theorems?

In Ebbinghaus' Mathematical Logic (2ed), in first order logic: It first proves IV.6.2 the correctness of sequent calculus on p70 (if I am correct, the soundness of sequent calculus); It then proves ...
1
vote
1answer
58 views

Half-SAT/ Half-Satisfiability

Is the following satisfiability problem hard? Given a set of clauses over boolean variables in conjunctive normal form, decide whether there is an assignment of truth values to the variables that ...
0
votes
0answers
37 views

What constraint am I missing for this SAT optimization problem?

I'm trying to solve a variation of the bin-packing problem. I have a certain floor space and I wish to place as many boxes as I can without stacking, i.e. if the floor is a 4 x 4 grid and I have one ...
0
votes
0answers
44 views

How can I prove the language 3COL is reducible to the language SAT?

3COL : Language describing all the possible ways of coloring a graph with three colors. SAT : Language describing all satisfiable boolean formulas. My goal is to demonstrate that 3COL $\leq_{p}$ SAT. ...
0
votes
0answers
17 views

SAT-Solver for default extensions

Assume I have written an algorithm to get a default extension of a normal default theory by employing a SAT solver that often terminates fast when the formula is satisfiable. My algorithm has the ...
1
vote
1answer
64 views

existence of a particular first-order sentence

A sentence is a first-order formula without any free variables. Let $A$ and $B$ be sets of first-order sentences such that $A\cup B$ is unsatisfiable (i.e. there does not exist a valuation that ...
1
vote
1answer
17 views

Inferring satisfiability of premise using natural deduction [closed]

Is there anyway to conclude whether the set of premises is satisfiable or not using the rules of natural deduction?
0
votes
0answers
13 views

Pure Real solutions in Linear Real Arithmetic theory of SMT

In SMT (satisfiability module theories) encoding, if one model a problem with Linear Arithmetic over Reals (LRA), is it possible to have Real (R) solution such that ...
1
vote
1answer
38 views

Conjunctive Normal Form evaluates true when atleast half of the clauses are true.

This is an Exam question. Which of the Following is TRUE about formulae in Conjunctive Normal form? -For any formula, there is a truth assignment for which at least half the clauses evaluate true. -...
2
votes
1answer
35 views

a set of sentences is satisfiable under two valuations iff every finite subset of it is satisfiable under two valuations [closed]

Let $\varGamma$ be a set of sentences. We say that HS($\varGamma$) if there are two valuations P1 and P2 such that for every $\theta$ $\in$ $\varGamma$: The value of $\theta$ under P1 is True or The ...
0
votes
1answer
42 views

How the upper bound is found in n-queens problem?

I am currently working on the queens problem defined as satisfiability problem. In the book I am following there is no explicit explanation how the upper bound is found (Q4 and Q5) to perform the ...
1
vote
0answers
39 views

Is Polarity of atoms in propositional formulae uniquely defined?

Given a propositional formula $\phi$, then positive/negative occurrence is defined as follows $\bullet$ $\phi$ occurs positively in $\phi$ $\bullet \neg \phi_1 $ occurs positively [negatively] in ...
0
votes
2answers
28 views

Expressing $n$ out of $m$ Boolean variables have to be true

I have a SAT problem with thousands of variables. Let $m$ be the number of variables. Each of the variables has $4$ indexes $v_{i,j,k,l}$. I struggle to find some concise mathematical notation to ...
0
votes
1answer
57 views

Question about SAT and assignment

We know that SAT is an NP problem, so having the answer "yes, it's satisfiable" or "no, it's not satisfiable" requires the work of a non-deterministic Turing Machine with Polynomial execution time. ...
2
votes
1answer
66 views

Help to understand the validness of relation in a model

In my assignment I have the following question: Find a model $M$ with domain $\{a, b, c, d\}$ so that: $M\vDash R(\overline{a},\overline{b})\land R(\overline{b},\overline{a})\land\neg Q(\overline{d})$...
0
votes
1answer
15 views

Why is this version of $k-SAT$ in $P$? [closed]

Why is this problem in $P$? Given a boolen polynomial $p$ with at most $k$ (positive integer $> 0$) clauses in CNF determine if $p$ is satisfable.
1
vote
1answer
37 views

About satisfiability when we know that there is at most one solution.

I was solving an awfully hard sudoku and at some point, the fact that there is exactly one assignment helped to exclude a number in some cell which helped me finishing it. This got me wondering in ...
0
votes
0answers
52 views

Propositional logic: entailment and satisfiability

I'm trying to prove the following result for formula $F$ and set of formulas $\mathcal{S}$: $\mathcal{S} \models F\Rightarrow \exists \mathcal{S}_0 ⊆ S$ (finite) such that $\mathcal{S}_0 \models F$ ...
2
votes
0answers
38 views

CNF-SAT is NP-complete if and only if CNF-UNSAT is co-NP-complete?

I have shown that a language $A$ is NP-complete $\iff$ its complement $\overline{A}$ is co-NP-complete. Also, I have shown that CNF-SAT is NP-complete. Since UNSAT is the complement of SAT, then ...
0
votes
1answer
31 views

Semantic Tableau First Order Satisfiability [closed]

I have just a short question: can I show satisfiability of a first order formula ∀x (Px ∨ Qx) → (∃x Qx ∨ ∀y Py) by using Semantic Tableau? In more general: if it ...

1
2 3 4 5 6