# Questions tagged [satisfiability]

Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

471 questions
Filter by
Sorted by
Tagged with
292 views

### Are there IP competitions?

Are there competitions for integer programming like there are for SAT and MAXSAT?
167 views

### Proof for NP-hardness of simultaneous minimization and maximization of a weighted subset

I am working on a problem defined as the following Given a set of $n$ elements called $R \subseteq \mathbb{N} \times \mathbb{N}$ and numbers $Z,G \in \mathbb{N}$, where $Z$ is a measure of our ...
20 views

### 2 SAT NL algorithm

How would you define the 2-SAT complement pseudo code? The information I gathered is, Let x be random variable chosen then we have to check if there exist a path between x to ~x and from ~x to x. If ...
34 views

### Does 2SAT contained in SAT?

Is it true that $2 S A T \subseteq S A T ?$ and in general is $k S A T \subseteq S A T$ where k is any positive integer is true? Thanks.
22 views

I have $m$ equations of the following form: $$x_1+x_2+\cdots+x_n=s,$$ where each variable is either 1 or 0, and the total number of variables is $m\approx3{,}000$. So I’m thinking of modeling each ...
44 views

### Complete resolution rule for 1-in-k SAT

In CNF SAT, each clause (A or B or C or...) must contain at least one true literal. The resolution rule applies to pair of clauses who have exactly one opposite literal. (A or B or C) and (!A or D ...
155 views

### Counting the number of satisfied models - given mathematical constraints

Question There are plenty of algorithms for solving the #SAT problem, with one being the DPLL algorithm and is implemented for all kinds of programming languages. As far as I've seen, they all take a ...
32 views

### Reference asking: phase transition in SAT

This is not a technical question, I hope this community has a room for such questions, but I will delete it in case this is inappropriate. It has been experimentally observed (e.g. here) that when ...
41 views

### What are the differences between symbolic execution and SAT solvers?

My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the ...
37 views

### When does Gaussian elimination solve exact 1-in-3 SAT?

Terms: A literal is a variable or its negation. A clause is a set of literals. An exact 3-in-1 clause is satisfied if an assignment of values to variables results in exactly 1 ...
16 views

### Translating running times of $3$-coloring to $k$-$SAT$ complexity

Suppose there is an $O(f(n))$ algorithm for $3$-coloring a graph on $n$ vertices what does it translate to in terms of time complexity for solving $k$-$SAT$ with $m$ clauses?
85 views

25 views

### Names of specific SAT variants

I enjoy reading research on satisfiability, but sometimes it's easier to find relevant information when you know the names of the variants. Example: All the clauses are width 3 and must have ...
65 views

### Turing reducibility of 2 versions of the satisfiability problem

I need help with this problem. There are 2 versions of the satisfiability problem:  decision version: determine whether an arbitrary formula f is satisfiable or not  search ...
62 views

### Reducibility of 2 boolean satisfiability problems

I beg some help with this problem. There are 2 boolean satisfiability problems. Problem $A$: Determining whether an arbitrary formula of size $n$ is $satisfiable$. Problem $B$: Determining ...
52 views

135 views

### Polynomial-time linear-reduction from Directed Hamiltonian Path Problem to 3SAT

Is there a polynomial-time reduction from Directed Hamiltonian Path Problem to 3SAT which is linear in the number of vertices? That is, it reduces every directed graph $G$ with $n$ vertices to a ...
255 views

### An Exact Method for Solving Small Instances of XORSAT

I have a couple of small instances for XORSAT for which I am to design and implement an exact method. However, there are a few catches. It is guaranteed that there always exists and answer but I need ...
83 views

### Class of languages recognizable by n-bit formulas of size at most $T(n)$

A Boolean (combinatoiral) circuit is a labeled (with the labels: AND, OR, NOT, IN, OUT), directed, acyclic graph, that satisfies: fan-in=2 for the AND and OR nodes fan-n=1 for the NOT nodes fan-...
64 views

### Give me ideas for an undergraduate final year math project about Boolean Satisfiability and SAT solvers

Context I am a student starting an undergrad math project. I was instructed to read Donald Knuth's Fascicle 6: Satisfiability and come up with ideas for a project from this material. I have 13 weeks ...
34 views

### Are there any resources or forums online for helping me understand TAOCP?

Context I am doing an undergrad math project that involves exploring Donald Knuth's "TAOCP, Volume 4, fascicle 6: Satisfiability". I am having trouble parsing some of this material. Surely ...
40 views

35 views

### CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P

CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P. I found this solution: We use the method of resolution to take the variables out ...
214 views

### CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number of literals, but at most one negated literal} ∈ P

The problem derived from the book of Sipser and the question was already posted (link) with partial comments. Let CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number ...
67 views

### Using induction prove that a K-SAT problem is NP-Complete

Using induction on k, how do I prove that the K-SAT problem is NP-complete? On wikipedia, it describes the Cook-Levin theorem to prove that K-SAT is NPC by reducting the K-SAT problem to a circuit-...
36 views

### CNF satisfiability with a bound on number of clauses

Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
126 views

### Are SAT problems with at most two false clauses NP-complete?

Is the problem of deciding whether a SAT instance, where at most two clauses are false (that is, any given variable assignment will either lead to all clauses being true, all but one, or all but two), ...
28 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 ..." ...
Given a 2SAT instance in CNF where each clause has at most two literals. Let $m$ be the number of clauses and $n$ be the number of variables et let $k$ be a positive number. Question: Is there a ...