# 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. ...
• 1,242
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"...
• 1,242
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

• 2,204
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 ...
• 1,537
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 ...
• 355
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 ...
• 103
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 ...
• 1
84 views

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. ...
• 154
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 ...
• 3,981
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-...
• 3,981
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 ...
• 109
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 ...
• 151
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 ...
• 1,850
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$ ...
• 13
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 ...
• 542
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 ...