# Questions tagged [satisfiability]

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

120 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
152 views

### Any Natural Problems shown Easy by Reduction to Horn SAT?

To show that a problem is polynomial-time solvable, an often-successful technique is to reduce it to 2SAT (that is the problem of deciding satisfiability of CNF formulas with every clause containing ...
184 views

### Approximate Weighted Partial Max SAT

Given a Weighted Partial Max SAT problem (WPM-SAT) - are there generally used algorithms or techniques to generate 'approximate' solutions, which are not necessarily optimal, but found faster than ...
• 313
45 views

### Benchmark of SAT solvers on random k-SAT instances at satisfiability threshold

I am looking for a solid reference (peer-reviewed publication) on the design and/or benchmarking of SAT solvers for random k-SAT ($4 \leq k \leq 8$) operating at satisfiability threshold. The majority ...
• 41
162 views

### Answer Set Program to SAT translation

During the presentation (a talk) Answer Set Programming: Boolean Constraint Solving for Knowledge Representation and Reasoning Torsten Schaub (University of Postdam) stated around twenty-one minutes ...
• 933
101 views

### What is the generating algorithm for the "komb" instances found on satcompetition.org?

For the 2017 and 2018 Random SAT Tracks of the SAT Competition ran by the International Conference on Theory and Applications of Satisfiability Testing there are small, yet difficult, random 3-SAT ...
69 views

### Is there a correspondence of steps between DPLL and sequent-calculus?

Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid? And given ...
• 263
77 views

### (Historical perspective) CSP and SAT inter-fertilization

[Disclaimer: this is a rather specialized question] It is known that techniques like Conflict-Driven Clause Learning (CDCL) and back-jumping -- which improved the Satisfiability (SAT) strategies ...
• 141
511 views

### How to encode reachability in a graph with walls as a SAT problem

Suppose we have a graph that represents a grid of cells. We are given a cell to start in and a cell that's the destination. There are cells that we cannot enter and they are known as walls. Finally we ...
• 155
255 views

### Determine if a graph has exactly 1 cycle using a SAT solver

I have a connected undirected graph whose edges are either enabled or disabled. I want to create a set of clauses that are SAT iff all enabled edges are part of a single loop. If I assert that each ...
54 views

### Is a "stacked", "local" version of 3-SAT NP-hard?

In this previous question, I learned that if each variable in a string $C \in 3\text{-SAT}$ appears only "locally", then finding a satisfying assignment is no longer NP-hard. My question below builds ...
• 319
243 views

### relationship between SAT and Min-ones SAT

If SAT can be decided in polynomial time, is it clear that Min-ones SAT can be decided in polynomial time? The idea I had was to take a poly decider of SAT and try it on a formula OR'd with all ...
• 181
702 views

### SAT and TSP Problems

I am trying to build a tool for solving TSP problem using a conversion to SAT. Does there exist an efficient conversion from the Travelling Salesman Problem to the Satisfiability problem? Since they ...
• 332
160 views

### Solving systems of boolean equations

So I have a system of equations where varibles range over $\{0,1\}$ and the only operation is logical or ($\lor$). Each equation is of the one of two forms 1) $a = b \lor c$ 2) $1 = a \lor b$ where ...
• 3,790
56 views

### Knowing if I have an optimal ordering for a OBDD

I'm learning about OBDD and I have learned that the size of a reduced OBDD (ROBDD) is dependent on the ordering of the variables, and that finding an optimal ordering is an NP hard problem. Say I ...
• 267
71 views

### Results on number of solutions to random 3-SAT?

I'm looking for some published results, either empirical or theoretical, on the number of solutions to random 3-SAT problems. Given $N$ variables and a clause-to-variable ratio $\alpha$, how does the ...
• 347
300 views

### "Balancing" positive and negative literals in 2-sat

I saw in an answer to this post that it is possible to construct 3-sat clauses with extra variables such that the number of positive and negative literals for each variable are equal. Does anyone ...
• 1,611
447 views

### smallest satisfiability-equivalent formulas (generalized Tseitin transform)?

What is known about the following optimization problem for formulas in propositional logic: input: formula $F$ output: formula $G$ in CNF with $\mathrm{Var}(G) \supseteq \mathrm{Var}(F)$ such that ...
356 views

### Satisfiabililty sufficient condition?

The conjecture itself: k-SAT formula is satisfiable if no pair of unit assignment $l$ and $\overline l$ imply the formula to contain unsatisfiable (k-1)-SAT. Example (XOR-SAT has no edges and cycles ...
• 1,429
46 views

• 326
1 vote