Skip to main content

Questions tagged [satisfiability]

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

130 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
7 votes
0 answers
167 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 ...
Dominik Peters's user avatar
6 votes
0 answers
190 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 ...
Matt D's user avatar
  • 313
6 votes
0 answers
89 views

Is it possible to reduce functional equations to SAT?

The problem of finding a solution for functional equations can be defined as: Let $A_0, A_1, A_2, \dots, A_n, B_0, B_1, B_2, \dots, B_n, X$ be terms of the $\lambda$-calculus, where all terms are ...
MaiaVictor's user avatar
  • 4,159
4 votes
0 answers
59 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 ...
sbbn's user avatar
  • 41
4 votes
0 answers
181 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 ...
Pushpa's user avatar
  • 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 ...
Sean Bearden's user avatar
4 votes
0 answers
70 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 ...
Alex's user avatar
  • 263
4 votes
0 answers
78 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 ...
ZakC's user avatar
  • 141
3 votes
0 answers
424 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 ...
Nicola Gigante's user avatar
3 votes
0 answers
276 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 ...
Gabe Burke's user avatar
3 votes
0 answers
57 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 ...
SapereAude's user avatar
3 votes
0 answers
280 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 ...
Drew Brady's user avatar
3 votes
0 answers
749 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 ...
RTK's user avatar
  • 332
3 votes
0 answers
165 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 ...
Jake's user avatar
  • 3,800
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 ...
Belgi's user avatar
  • 267
3 votes
0 answers
72 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 ...
Andrew's user avatar
  • 347
3 votes
0 answers
312 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 ...
Ari's user avatar
  • 1,631
3 votes
0 answers
450 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 ...
d8d0d65b3f7cf42's user avatar
3 votes
1 answer
367 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 ...
rus9384's user avatar
  • 1,781
2 votes
0 answers
37 views

Satisfiability of a boolean formula with two occurrences of each variable with a special ordering

I am interested in the complexity of a special case of the boolean satisfiability problem: We are given a boolean formula, consisting only of the logical operators $\land$ and $\lor$ (that can be ...
SimonNW's user avatar
  • 161
2 votes
0 answers
76 views

Monotone boolean satisfiability problem : finding minimal solutions

I am very interested in the following questions, which sprang out from the topological study of loops in surfaces and their intersection numbers. Consider, over a finite set of boolean variables $X$, ...
Christopher-Lloyd Simon's user avatar
2 votes
0 answers
62 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 $...
vvg's user avatar
  • 135
2 votes
0 answers
41 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 ...
Thomas Tappeiner's user avatar
2 votes
0 answers
32 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 ...
No one's user avatar
  • 21
2 votes
0 answers
73 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 ...
Geremia's user avatar
  • 154
2 votes
0 answers
44 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 ...
Dan D-man's user avatar
  • 534
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 ...
Albert Hendriks's user avatar
2 votes
0 answers
82 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 -- ...
dnes's user avatar
  • 121
2 votes
1 answer
114 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 \...
Fearvik's user avatar
  • 21
2 votes
0 answers
614 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$ ...
Joey's user avatar
  • 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 ...
user avatar
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-...
Dudi Frid's user avatar
  • 231
2 votes
0 answers
174 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 ...
Troy McClure's user avatar
2 votes
0 answers
29 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 ...
Mathieu Mari's user avatar
2 votes
0 answers
65 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 ...
Russell Easterly's user avatar
2 votes
0 answers
188 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, ...
Joey Eremondi's user avatar
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 ...
Albert Hendriks's user avatar
2 votes
0 answers
389 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 ...
Manuel Lafond's user avatar
2 votes
0 answers
41 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 ...
TomR's user avatar
  • 1,401
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$. ...
matheuscscp's user avatar
1 vote
0 answers
17 views

"package" compatibility solver with verion ranges

I am looking for how to solve the package compatibility problem. I have found some relevant research and libraries. But some of them are older. I am wondering if there is any more recent research and ...
wilx's user avatar
  • 111
1 vote
0 answers
15 views

Are there ASICs optimized to solve the SAT problem?

Are there ASICs (application-specific integrated circuits) optimized to solve the SAT problem, such as by the DPLL algorithm?
Geremia's user avatar
  • 154
1 vote
0 answers
90 views

Sat solvers with backdoor set

I have large cnf with thousands of variables, but with known compact backdoor set. I think this set can be used by CDCL solvers to choose assignment variables to simplify formula much faster, but I ...
Alexey Kholodkov's user avatar
1 vote
0 answers
23 views

CNF Horn-renamability to 3-CNF Horn-renamability reduction?

A CNF formula is Horn-renamable if you can invert variables in such a way that each clause has at most one positive literal. There is an algorithm based on a reduction to 2-SAT given in Renaming a Set ...
rus9384's user avatar
  • 1,781
1 vote
0 answers
24 views

Are there any SAT outside of $\mathsf{RP}$ variants that are solvable in quasipolynomial time?

It's possible to construct SAT problems that are solvable in quasipolynomial time, but they are also solvable in polylogarithmic space. Consider, for example, the following problem: Let a set $S$ ...
rus9384's user avatar
  • 1,781
1 vote
0 answers
22 views

SAT for clauses of the form "At most m out of n are false"

Recall some terminology: Let $\mathsf P$ be a finite set of propositional atoms, and let $\Phi$ be a proposition over $P$ that is generated from $\top$, $\bot$, $\neg$, $\wedge$, and $\vee$. Then: A ...
Jim's user avatar
  • 111
1 vote
1 answer
94 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 ...
Tilo RC's user avatar
  • 11
1 vote
0 answers
44 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 ...
Soha's user avatar
  • 25
1 vote
0 answers
63 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....
Freshman's Dream's user avatar
1 vote
1 answer
102 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. ...
Vivek Joshy's user avatar