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
7
votes
0
answers
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 ...
- 363
6
votes
0
answers
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 ...
- 313
4
votes
0
answers
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 ...
- 41
4
votes
0
answers
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 ...
- 923
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
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 ...
- 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
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 ...
- 155
3
votes
0
answers
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 ...
- 31
3
votes
0
answers
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 ...
- 319
3
votes
0
answers
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 ...
- 181
3
votes
0
answers
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 ...
- 332
3
votes
0
answers
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 ...
- 3,760
3
votes
0
answers
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 ...
- 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
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 ...
- 1,601
3
votes
0
answers
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 ...
- 141
3
votes
1
answer
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 ...
- 1,393
2
votes
0
answers
42
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
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 ...
- 121
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 ...
- 21
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 ...
- 155
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 ...
- 494
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,450
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 -- ...
- 121
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 \...
- 21
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 ...
- 448
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$ ...
- 53
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 ...
- 673
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-...
- 151
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 ...
- 624
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
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 ...
- 341
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, ...
- 29.5k
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,450
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 ...
- 530
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 ...
- 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
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....
- 133
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. ...
- 111
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 ...
- 65
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$ ...
- 413
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=b$ $mod$ $2$. Solvability (i.e. ...
- 11
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 ...
- 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
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 ...
- 23
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 ...
- 71
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(...
- 219
1
vote
0
answers
60
views
How often can a learned clause cause this solver to backtrack?
The is an improvement to the X3SAT solver I described in What is wrong with this simple proof of P=NP? I have fixed the flaw found in that solver. Now, I want to know how often the solver described ...
- 341
1
vote
0
answers
53
views
Different definitions of Exponential Time Hypothesis
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 ...
- 2,923