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
1 vote
0 answers
17 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 ...
user avatar
0 votes
1 answer
33 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. ...
user avatar
  • 1,242
0 votes
0 answers
10 views

Better at_most_k SAT encoding

I am trying to find and implement a good algorithm for encoding the at_most_k operator in SAT clauses. I read this paper "Yet Another Comparison of SAT Encodings for the At-Most-K Constraint"...
user avatar
  • 1,242
0 votes
1 answer
32 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 (...
user avatar
0 votes
0 answers
15 views

Number of distinct unsatisfiable 3CNF formula consisting of n variables

I'm interested to know if anyone knows the number of unsatisfiable 3SAT formulae in CNF consisting of $n>3$ variables. Specially, formulae where no clause contains the same literal twice, either ...
user avatar
1 vote
1 answer
66 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 ...
user avatar
1 vote
1 answer
34 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]\...
user avatar
  • 49
2 votes
0 answers
56 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 $...
user avatar
0 votes
1 answer
51 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 ...
user avatar
2 votes
1 answer
73 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 (...
user avatar
0 votes
1 answer
54 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
53 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
5 votes
1 answer
99 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
21 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-...
user avatar
  • 133
0 votes
2 answers
35 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 ...
user avatar
5 votes
2 answers
216 views

Kees Doets's definitions of logical consequence

everyone, I'm reading Kees Doets's Basic Model Theory (which is freely and legally downloadable from https://web.stanford.edu/group/cslipublications/cslipublications/Online/doets-basic-model-theory....
user avatar
0 votes
0 answers
32 views

Show $I\Vdash_{\Sigma} φ$ iff $I\Vdash_{\Sigma} \forall x φ$.

Let $\Sigma$ be a signature (decidable, with equality) and $I$ an interpretation structure over said signature. Let $φ$ be a formula. Show $I\Vdash_{\Sigma} φ$ iff $I\Vdash_{\Sigma} \forall x φ$. ...
user avatar
0 votes
1 answer
24 views

what does p in "3-CNF-SAT ≤p SUBSET-SUMS" mean?

I come across this notation from book "Introduction to Algorithm, CLRS", page 1097, but have no idea why p is subscript Another source: https://www.youtube.com/watch?v=i8Kt9IBZ8FU
user avatar
-1 votes
1 answer
128 views

Checking tautology

Given a Boolean formula $\phi$ in CNF form, I'll check whether there exists a clause that can be falsified i.e. check for literals of the form $x \vee \neg x$. If there are not any such literals in a ...
user avatar
0 votes
0 answers
76 views

Are two formulae $\phi = p, \psi = \neg p$ equisatisfiable?

Two formulae $\phi$ and $\psi$ are equisatisfiable if both of them are satisfiable or none of them is satisfiable. And they can have their own independent truth assignments $\tau_{1}$ and $\tau_{2}$ ...
user avatar
1 vote
0 answers
113 views

Is (3,3)-NAE-SAT NP-complete?

In this question I assume the following: in either $(i,j)$-SAT or $(i,j)$-NAE-SAT, every clause has exactly $i$ literals, and a given variable appears at most $j$ times in the entire formula. NAE ...
user avatar
  • 59
5 votes
1 answer
99 views

prove or disprove: every non satisfiable set of WFF has a non satisfiable sub set such every proper subset of it is satisfiable

Let $\Gamma$ be a non-satisfiable set of well-formed formulas (wff). prove or disprove: $\Gamma$ has a non-satisfiable subset $\Delta\subseteq\Gamma$ such that for every $\phi\subsetneq\Delta$ is ...
user avatar
2 votes
1 answer
137 views

If the length plus the width of rectangle ABCR is 8, then find perimeter of circle given rectangle is in a circle

In the figure, arc SBT is one quarter of a circle with center R and radius $6$. If the length plus the width of rectangle ABCR is $8$, then find the perimeter of the shaded region. Background: This is ...
user avatar
0 votes
0 answers
27 views

How can one show that, in first-order logic, the validity or satisfiability of a formula in a domain depends only on the cardinality of the domain?

I'm pretty much stuck at the beginning. I thought I might try doing it by induction on the length of the formula, but I have no clue how to get started even on the atomic case. (I am aware that a ...
user avatar
  • 31
0 votes
0 answers
9 views

How would we quickly and simply determine if by recycling items into categories of different resources, we can reach a certain target?

Context In a game system, there are various items that can be broken down into the core resources of the game, $\{r_i\}$. For the system case I'm interested in, there are $5$ core resources. $$ r_1, ...
user avatar
  • 2,204
0 votes
0 answers
29 views

Systems of linear homogenous inequalities: getting started

I have a number of questions of varying difficulties related to satisfying largish (as large as possible) systems of linear inequalities. I gather these aren't easy, so I'd be happy to get numerical ...
user avatar
  • 1,537
0 votes
0 answers
89 views

Implication graphs and 2-SAT

I'm a computer science student and I recently got into complexity theory and I'm having a hard time wrapping my head around some of the topics, so I thought I would try to solve some of exercises in ...
user avatar
  • 355
0 votes
1 answer
37 views

if for every finite statement set is satisfiable by 2 then any statement set is satisfiable by 2

Let S be a statement set of first order logic. We say that it is satisfiable by 2 if one can split to 2 the set, so each set is satisfiable . Prove or disprove, if every finite is satisfiable by 2, ...
user avatar
0 votes
0 answers
19 views

Complexity of representing all satisfying assignments

I am not formally educated in Complexity Theory hence asking this question. In which complexity class should the problem of representing all satisfying assignments of a Boolean system (equivalently a ...
user avatar
0 votes
0 answers
36 views

Show that sentence $ ∃x∀y∃z((F(y, z) → F(x, z)) → (F(x, x) → F(y, x))) $ is true in every finite model but it is not a valid formula

∃x∀y∃z((F(y, z) → F(x, z)) → (F(x, x) → F(y, x))) How can I show for this formula that it is true in every finite model but it isn't a valid formula? Can someone please help me solve this problem/send ...
user avatar
  • 1
0 votes
0 answers
84 views

Show if the IS is NP-Complete

Let $G = (V, E)$ be an undirected graph. A subset $I \subseteq V$ of the vertices in $G$ is an independent set if no two vertices $u, v \in I$ are adjacent in $G$, i.e., for any $u, v \in I$, we have $...
user avatar
  • 1
0 votes
0 answers
73 views

Validity in First Order Logic

I am really confused with validity in First Order Logic. Which is the difference between: $(\exists x)Fx$ being valid and $(\forall x)Fx$ being valid? Does the second one imply the first one? Any ...
user avatar
  • 141
0 votes
1 answer
41 views

HORN algorithm - clarity needed

I have been spending some time studying the HORN algorithm, but my textbook, as well as most posts online, are quite vague around the steps taken. These are the steps from my textbook: My questions: ...
user avatar
1 vote
0 answers
42 views

Constructing a Hamiltonian cycle for 6-dominos

This may be the wrong forum, as it's sort of about programming also. I'm trying to encode a directed Hamiltonian cycle for a standard set of 28 6-dominos. The difficulty I am having is trying to keep ...
user avatar
  • 173
2 votes
0 answers
38 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-...
user avatar
  • 141
2 votes
1 answer
661 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 ...
user avatar
0 votes
1 answer
212 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 ...
user avatar
  • 1,211
3 votes
1 answer
71 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 $\...
user avatar
4 votes
2 answers
148 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....
user avatar
6 votes
1 answer
387 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. ...
user avatar
  • 154
2 votes
1 answer
175 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 ...
user avatar
  • 3,981
3 votes
2 answers
61 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-...
user avatar
  • 3,981
0 votes
0 answers
30 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 ...
user avatar
  • 109
1 vote
0 answers
39 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 ...
user avatar
  • 151
0 votes
1 answer
88 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 ...
user avatar
  • 1,850
0 votes
0 answers
70 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$ ...
user avatar
  • 13
1 vote
0 answers
24 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 ...
user avatar
0 votes
1 answer
121 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 ...
user avatar
  • 542
0 votes
1 answer
65 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 ...
user avatar
0 votes
1 answer
35 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 ...
user avatar

1
2 3 4 5 6