# Questions tagged [satisfiability]

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

113 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
150 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 ...
177 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 ...
28 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 ...
147 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 ...
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 ...
66 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 ...
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 ...
455 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 ...
217 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 ...
53 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 ...
225 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 ...
664 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 ...
154 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 ...
53 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 ...
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 ...
294 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 ...
440 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 ...
348 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 ...
42 views

In Boolean Satisfiability of CNF formulae we have $k$-SAT where each clause has at most $k$ literals. It is well known that $k$-SAT is polynomial time reducible to $3$-SAT. It is also well known that $... 2 votes 0 answers 33 views ### Problems with proof of NP-completness of SAT following Cooks original paper I am currently in the process of trying to understand the original proof of NP-completeness of SAT given in the seminal paper by Cook [COOK71] and have struggled with a few of the details of the proof ... 2 votes 0 answers 30 views ### Reductions from 3-SAT that won't work directly from SAT Our prof talked about why it's good to know that 3-SAT is NP-complete because it's easier to craft reductions from it than from plain SAT. However, all the examples we've seen (reduction to ... 2 votes 0 answers 49 views ### Quantum Boolean SAT algorithm? Is there a quantum SAT algorithm, a quantum analogue of the DPLL or CDCL algorithms? Note: I'm not looking for the quantum analogue of the Boolean satisfiability problem (though that would be ... 2 votes 0 answers 34 views ### Non-trivial reduction form SAT to$3$-SAT Looking for any idea for reduction from$SAT \leq 3-SAT$where$SAT$is known to have$d$variables at most in each clause. I am looking for a reduction in which the resulting formula will not depend ... 2 votes 0 answers 38 views ### Under ETH:$\exists$Problem unsolvable in$2^{o(n)}\Leftrightarrow^?$3-SAT can be represented in linear bits It is a popular open question if there is a problem unsolvable in$2^{o(n)}$on inputs with$n$bits, assuming ETH. I recommend reading that question first. That question states that, assuming the ETH ... 2 votes 0 answers 41 views ### Necessary condition for 3-CNF unique satisfiability I need to iterate through all formulas of 7 variables in 3-CNF which have unique satisfying assignment (1,1,1,1,1,1,1). I could iterate through all formulas which are true under that assignment -- ... 2 votes 1 answer 82 views ### Proving satisfiability using resolution and variable elimination I don't 100% understand this. But I have a entailment, and I want to prove whether it is satisfiable or not, and I will do this using resolution and variable elimination. Here is the formula:$$(x_1 \... 2 votes 0 answers 166 views ### Test suite for SAT solvers I'm looking for a collection of SAT problems that are usable for a test suite, i.e.: are small/easy to solve, that is, this is not a benchmark but a correctness test suite some satisfiable, some ... 2 votes 0 answers 399 views ### Reducing Dominant Set Problem to SAT I am trying to solve a problem and I am really struggling, I would appreciate any help. Given a graph$G$and an integer$k$, recognize whether$G$contains dominating set$X$with no more than$k$... 2 votes 0 answers 43 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 ... 2 votes 0 answers 88 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-... 2 votes 0 answers 159 views ### Second Order QBF Consider a universe with two elements 0,1 and a second order formula, i.e. of the form "forall R exists S ... such that F", where R,S are relation symbols of some given arity, and F is some first ... 2 votes 0 answers 28 views ### Inapproximability result for a special version of 1-in-kSAT Max 1-in-kSAT is the following maximisation problem : Given$n$variables$x_1,\dots,x_n$, and$m$clauses$C_1, \dots, C_m$, find a valuation such that the number of clauses satisfied by exactly one ... 2 votes 0 answers 59 views ###$X_3SAT$Loop Reductions Exactly$1$-in-$3$SAT ($X_3SAT$) is a variant of the Boolean satisfiability problem. Given a set of clauses, each clause having three literals, is there a set of literals such that each clause ... 2 votes 0 answers 168 views ### Passing arrays vs functions as arguments in SMT? In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ... 2 votes 0 answers 58 views ### substituting expressions I have a set of expressions$E_1 .. E_n$over boolean variables and I'm looking for an assignment to the variables so that all expressions are satisfied. Normally this would be NP-complete, but I ... 2 votes 0 answers 311 views ### Is Max-2SAT with exactly 3 occurrences per variable APX-hard? The Max-2SAT problem asks if at least k clauses of a 2CNF formula can be satisfied. The Max-2SAT(at-most-3) problem is the restriction in which every variable occurs in at most 3 clauses (counting ... 2 votes 0 answers 34 views ### BDI logic or KARO framework solver - are there solvers for any new logic? I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ... 2 votes 0 answers 2k views ### DPLL time complexity analysis Consider the most naïve backtracking for CNF-SAT. It only checks if an assignment satisfies the input formula$\phi$when all the$n$variables have values assigned. Let$m$be the size of$\phi$. ... 1 vote 0 answers 34 views ### Restricted Planar 3-SAT NP-hard As we all know, 3-SAT is NP-hard. Two of the less known results are that Planar 3-SAT is NP-hard and also a 'restricted' 3-SAT, where any literal appears in at most two clauses turns out to be NP-hard.... 1 vote 1 answer 55 views ### Is there an SMT/SAT algorithm for General Predicate Logic (FOL)? I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ... 1 vote 0 answers 90 views ### CNF – satisfy at most a fixed number of clauses I'm working on this task: Prove that the following problem can be solved in time$2^{k} \cdot \Vert \varphi \Vert^{\mathcal{O}(1)}$: given a boolean formula$\Vert \varphi \Vert$in CNF, decide ... 1 vote 0 answers 40 views ### Probability of a randomised algorithm solving SAT Let WALKSAT be defined as follows: Let$σ$be a random truth assignment to the vars For$t = 1, 2, . . . , 3n$: ◦ If$\phi$is satisfied by$σ$, exit the loop ◦ Else, pick an unsatisfied clause$c$... 1 vote 0 answers 117 views ### Is there an alternative method to using Gaussian elimination in order to solve 3-XORSAT I have a large system of$3$-$XORSAT$constraints (i.e. up to$3$variables per constraint) and this can be represented in matrix form as a linear algebra problem$Ax=bmod2$. Solvability (i.e. ... 1 vote 1 answer 115 views ### Best compression algorithm for CNF SAT instances in DIMACS For a CNF SAT instance in the DIMACS format what is the best algorithm to compress it? What is the best algorithm for 3-SAT instances in particular? In 2020 SAT competition used .xz which if I ... 1 vote 0 answers 22 views ### Software/library to generate Ising models for random$k$-sat problems Could someone point me to a software/library which lets one to generate the Ising model/spin model for random$k$-sat problems or$k$-sat problem of a given structure? I understand that it will be ... 1 vote 0 answers 70 views ### How to design an unbounded Monte Carlo algorithm for SAT(Boolean Satisfiability Problem) problem? I want the algorithm to be in polynomial time and the correct answer rate is 0.5 or more. (True / false judgment is polynomial time) All the methods I think of take exponential time(2^n). Can anyone ... 1 vote 0 answers 140 views ### Which features can be considered for neural network based SAT solving? I'm trying to implement SAT solver, based on backtracking algorithm and BCP. This SAT solver is trying to pick one literal from each clause, from 3-CNF SAT instances. I've implemented a neural network ... 1 vote 0 answers 121 views ### Reduction between Parity-SAT and approximate counting Consider two problems as defined here. Approximate counting: Given a Boolean function$f(x)$, for$x \in \{0, 1\}^{n}$, distinguish between the two cases: The number of satisfying assignments for$f(...
1 vote
I am reading basics of Exponential Time Hypothesis (ETH). There are two statements for it: Statement 1 There exists no $2^{o(n)}$ algorithm for $3$-SAT, where $n$ is the number of variables. Statement ...