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
7
votes
0
answers
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 ...
- 363
6
votes
0
answers
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
4
votes
0
answers
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
4
votes
0
answers
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
4
votes
0
answers
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 ...
- 91
4
votes
0
answers
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
4
votes
0
answers
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
3
votes
1
answer
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
3
votes
0
answers
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 ...
- 31
3
votes
0
answers
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
3
votes
0
answers
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
3
votes
0
answers
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
3
votes
0
answers
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
3
votes
0
answers
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
3
votes
0
answers
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
3
votes
0
answers
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
3
votes
0
answers
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 ...
- 141
3
votes
1
answer
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
2
votes
0
answers
46
views
Modified DPLL for 3-SAT by reducing to 2-SAT
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 $...
- 135
2
votes
0
answers
36
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 ...
- 121
2
votes
0
answers
31
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 ...
- 21
2
votes
0
answers
61
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 ...
- 142
2
votes
0
answers
35
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 ...
- 494
2
votes
0
answers
41
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,469
2
votes
0
answers
48
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 -- ...
- 121
2
votes
1
answer
97
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 \...
- 21
2
votes
0
answers
255
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 ...
- 448
2
votes
0
answers
418
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$ ...
- 53
2
votes
0
answers
44
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 ...
user102180
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-...
- 161
2
votes
0
answers
169
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 ...
- 634
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 ...
- 356
2
votes
0
answers
62
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 ...
- 341
2
votes
0
answers
180
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, ...
- 29.7k
2
votes
0
answers
59
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,469
2
votes
0
answers
347
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 ...
- 530
2
votes
0
answers
35
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 ...
- 1,381
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$. ...
- 325
1
vote
0
answers
48
views
How to find the learned clause from a UIP cut
I would guess that this question is going to make some people wonder how I haven't already found a solution looking through papers -- but I do not see a clear algorithm.
In implementing CDCL, I read ...
- 33
1
vote
1
answer
66
views
A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?
I am working on an LRA Theory solver for SymPy, an open source python library for symbolic computations. You can find my work here. Currently I'm trying to optimize it to run faster.
My implementation ...
- 11
1
vote
0
answers
30
views
Shortest unsatisfiable 3-CNF that can't be refuted with narrow resolution?
Proof width (the size of the largest clause in a proof) plays an important part in refuting an unsatisfiable formula. If a formula has a bounded-width resolution proof of its unsatisfiability, then ...
- 25
1
vote
0
answers
54
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....
- 133
1
vote
1
answer
80
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. ...
- 111
1
vote
0
answers
108
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 ...
- 65
1
vote
1
answer
65
views
Logical Consequence - Equivalent Assertions
I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
- 11
1
vote
0
answers
41
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$ ...
- 423
1
vote
0
answers
157
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=b$ $mod$ $2$. Solvability (i.e. ...
- 11
1
vote
1
answer
141
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 ...
- 11
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 ...
- 326
1
vote
0
answers
80
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 ...
- 23