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

295 questions
Filter by
Sorted by
Tagged with
1 vote
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 ...
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. ...
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"...
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 (...
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 ...
1 vote
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 ...
1 vote
34 views

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 ...
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 (...
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 ... 53 views

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 ...
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 ...
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, ...
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 ...
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 ...
84 views

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 $... 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 ... 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: ... 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 ... 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-... 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 ... 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 ... 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$\... 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....
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. ...
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 ...
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-...
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 ...
1 vote
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 ...
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 ...
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$ ...
1 vote
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 ...
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 ...
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 ...
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 ...