Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

Filter by
Sorted by
Tagged with
0 votes
0 answers
10 views

Finding a common variable value among all SAT solutions

Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
csaltachin's user avatar
0 votes
0 answers
9 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
  • 148
1 vote
1 answer
140 views

SAT solvers for counting the number of solutions

Are there existing SAT solver libraries that can count the number of solutions of a boolean formula? Can you give examples? I mean implementations more efficient than the naive approach, i.e. each ...
Fabius Wiesner's user avatar
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
1 answer
321 views

How fast can we make generalized k-SAT?

Suppose a generalized version of k-SAT where the usual clauses (disjunctions of literals) are generalized to arbitrary Boolean functions of k variables. (For example, $(x \oplus (y \land z)), ((x \...
A. H.'s user avatar
  • 498
1 vote
1 answer
117 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 ...
Jack Sack's user avatar
1 vote
1 answer
44 views

Showing SAT is auto-reducible

I am trying to wrap my head around the concepts of auto-reducibility and having access to an Oracle. The way I understand is that a language is auto-reducible iff there is a Turing Machine $M^{L}(x)=1$...
Meki21's user avatar
  • 93
1 vote
1 answer
100 views

Specialized SAT solver (?)

(Context) Given two byte arrays of length 16, say $L$ and $H$, one can define a mapping $M$ from the set of all bytes to itself in the following way. If $0 \le b \lt 256$ is a byte, let $\text{lo}(b)$ ...
fuzzypixelz's user avatar
3 votes
1 answer
88 views

Could SAT solvers be significantly more efficient if they allowed for non-CNF formula?

SAT Solvers focus on CNF formulas. For many implications it is much mroe natural to use implications and conjunctions to encode problems, and when converting to CNFs, information is lost, and the ...
user56834's user avatar
  • 3,752
0 votes
0 answers
13 views

Reference request for Unit Clause Based SAT Reduction Rules

I tested my XSAT solver using the 4 pigeons in 3 holes problem converted to XSAT. The pigeon hole instance I give below had 108 variables and 88 clauses after being converted to monotone XSAT. My ...
Russell Easterly's user avatar
0 votes
0 answers
17 views

Complexity Class of the Problem: Existence of Unsatisfying Interpretations in Boolean Formulas

What is the complexity class of the problem if there exist two different interpretations that do not satisfy a given Boolean formula? I believe the problem of existence of an interpretation that does ...
Lupital's user avatar
0 votes
1 answer
56 views

What's the relation between DPLL and BDDs?

BDDs are a way of representing Boolean formulas. DPLL is an algorithm to determine satisfiability of Boolean formulas. My understanding is that the two are used for SAT solving. How are they combined?
user1868607's user avatar
  • 2,194
1 vote
1 answer
52 views

CDCL SAT solvers and don't cares

Modern CDCL SAT solvers often can return partial assignments where missing literals mean that the value of that variable is not important for the satisfaction of the formula (i.e. it is a don't care). ...
Nicola Gigante's user avatar
4 votes
0 answers
52 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
2 votes
0 answers
61 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
-1 votes
1 answer
47 views

Can you help me find some examples of 3co-SAT for 4 variables?

I've been studying the examples of 3co-SAT recently. It's easy to find an example of one variable. $(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$ Examples of 2 ...
lz9866's user avatar
  • 315
2 votes
2 answers
125 views

what does **input** mean for the $3SAT$ question? Is it the number of variables $n$ or the number of clauses $m$

We know that $3SAT \in NP$, and the definition of $NP$ is as follows: $NP$ is the class of languages that have polynomial time verifiers. But I have a question: what does input mean for the $3SAT$ ...
lz9866's user avatar
  • 315
0 votes
1 answer
404 views

Time-complexity of evaluating a CNF formula

Given a Boolean formula over $n$ variables in CNF and a partial assignment to it, all the algorithms I can think of to evaluate the assignment run in time $\Theta(n^2)$. Is it possible to do it in $O(...
Noel Arteche's user avatar
1 vote
1 answer
190 views

MAX-SAT 2-Approximation algorithm

I have the two following questions: I know SAT -> MAX-SAT but how can I show that if MAX-SAT is solved in polynomial time then SAT is solved in polynomial time as well?(I guess using approximation ...
kostger's user avatar
  • 37
1 vote
1 answer
80 views

prove that if $SAT\notin Size(2^{n/100})$ then CorrectSATSolver$\in P$

I need to prove that if $SAT\notin Size(2^{n/100})$ then CorrectSATSolver$\in P$. Where CorrectSATSolver $= \{C | C(\varphi) = 1 \iff \varphi$ is satisfiable$\}$. In other words, CorrectSATSolver ...
ORN's user avatar
  • 23
4 votes
1 answer
656 views

What are efficient approaches to implement unit propagation in DPLL-based SAT solvers?

I'm trying to decompose deduction steps of DPLL algorithm -- unit propagation and pure literal elimination -- for parallelization. However, I want a baseline and asymptotic analysis to compare to my ...
vixrant's user avatar
  • 43
2 votes
0 answers
70 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
  • 148
2 votes
1 answer
104 views

How to determine if clause will change the satisfiability of the 3SAT formula?

I have satisfiable 3SAT formula like: (x1 or x2 or x3) and (not x1 or x2 or not x3) and some clause which is not in this formula ...
Alexandr Dorofeev's user avatar
3 votes
1 answer
78 views

Stalmarck's method: x ≡ x → z, does z have to be true?

I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that: y $\to$ z $\equiv$ x where x, y and z are booleans which ...
Leop's user avatar
  • 53
2 votes
0 answers
42 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
  • 514
6 votes
1 answer
176 views

Why is this SAT problem hard and what can I do about it?

For a graph theory problem I need to solve hundreds of millions of CNF problems that typically have around 200 variables and 15,000 clauses no larger than 10. By default I use glucose, which usually ...
Brendan McKay's user avatar
1 vote
1 answer
149 views

Three dimensional matching expressed as SAT

The posting in the website Embedding SATISFIABILITY into 3-DIMENSIONAL MATCHING seeks $3SAT$ as a $3$ dimensional matching instance. I am looking to solve the converse problem. How to solve three ...
Turbo's user avatar
  • 2,891
0 votes
0 answers
57 views

SAT solvers that can compute prime implicants and/or minimization

I'm looking into computing the prime implicants of a Boolean function. I have found many different algorithms in the literature, many of them relying on SAT solvers. However, I have not been able to ...
Noel Arteche's user avatar
1 vote
0 answers
151 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 ...
komorra's user avatar
  • 71
1 vote
1 answer
242 views

Proving using a SAT solver that KB entails D

Suppose you're given this KB: $$KB = (A, A ⇒ B, A ⇒ C, B ∧ C ⇒ D)$$ How would you show using a SAT solver that $KB \vDash D$?
Manny's user avatar
  • 13
1 vote
0 answers
65 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 ...
Russell Easterly's user avatar
2 votes
1 answer
64 views

Solving largely monotone SAT formulas

I just wonder if solving largely monotone SAT formulas (meaning most clauses do not contain negated literals, but some do) is in any way easier than general SAT formulas? In other words, are there ...
apen's user avatar
  • 369
1 vote
2 answers
497 views

Is there any algorithm for 3SAT problem that is fast and relatively easy to implement?

Here is the description for 3SAT satisfiability problem. I already know about the DPLL algorithm, but it's implementation is pretty complex. I would like some algorithm that is relatively simpler but ...
Shaif Chowdhury's user avatar
3 votes
1 answer
50 views

How to leverage the fact that I'm solving 1000's of very similar SMT instances?

I have a core SMT solver problem consisting of 100,000 bit-vector array clauses, and one 10000-dimensional bit-vector array. Then, my program takes as input k << 100,000 new clauses, and adds ...
lightning's user avatar
  • 225
12 votes
4 answers
2k views

Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
Omar Shehab's user avatar
2 votes
1 answer
96 views

Find a list of actions that result in desired state

I have a problem that I need to solve, and I'm looking for which area of computer science (algorithms. etc) would be appropriate to solve this problem. In the system we have a list of actions that a ...
user1647947's user avatar
1 vote
1 answer
920 views

What are the differences between symbolic execution and SAT solvers?

My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the ...
Paul Razvan Berg's user avatar
3 votes
1 answer
136 views

Clarification on "clause learning" in DPLL algorithm

I am struggling to understand the idea of conflict-driven clause learning, in particular, I can not understand why the clause we 'learned' is a substantially new (i.e. the clause database does not ...
Vladislav's user avatar
  • 687
4 votes
2 answers
460 views

Is it feasible to solve this subset cover problem with SAT solver?

The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied: if $S \subseteq \mathcal{S}$ then $|S|=6$; for any $A \subseteq \{1,...
NonalcoholicBeer's user avatar
3 votes
1 answer
187 views

CNF satisfiability with a bound on number of clauses

Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
Ozzy's user avatar
  • 131
3 votes
1 answer
887 views

Practical hard 3-sat instances

The $3-SAT$ problem is known to be NP-complete problem. Which means that (as far as I understand), unless $P \neq NP$, for every algorithm $A$ which decides $3-SAT$, $A$ runs in super polynomial time (...
Jonathan's user avatar
2 votes
1 answer
131 views

Non-Boolean SAT

I was wondering about the complexity of SAT tests with variables $x_i = 0 \lor 1 \lor 2 \dots \lor n$, with clauses being of the form $x_i = a \implies x_j \neq b$. When $n=2$, we have 2SAT, which has ...
Zach Hunter's user avatar
7 votes
1 answer
892 views

Random restarts for unsatisfiable instances

In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice. ...
rwallace's user avatar
  • 386
1 vote
2 answers
166 views

Can an optimization algorithm be "universal"?

I am wondering if a Bayesian Optimization framework (e.g. Google's Vizier) can be used in lieu of a traditional solver like Gurobi or CPLEX. In trying to answer this question, I realized that I don'...
Sasha the Noob's user avatar
3 votes
1 answer
335 views

Sum of unique integers to cnf constraint

As a study project I try to solve the kakuro puzzle problem using SAT SOLVER. I can't really find an efficient way to convert the sum of k unique integers (1...9) to a CNF constraint. What I had in ...
misha312's user avatar
  • 209
1 vote
1 answer
127 views

Encoding a "not-k-out-of-n" constraint for SAT solvers

I'm finding myself needing to encode a "not-k-out-of-n" constraint in a SAT solver. The "at-most-k-out-of-n" constraint for SAT solvers is something I can find research about -- this paper by Frisch ...
onigame's user avatar
  • 203
3 votes
0 answers
274 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
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
2 votes
1 answer
48 views

Translation of diagnosis problem to SAT

I have the following diagnosis problem: h(A): z1 = not(in1) h(D): z2 = not(in2) h(B): z3 = z1 or z2 h(C): out1 = not(z3) h(E): out2 = not(z3) This is an image of the system: I have an observation ...
erap129's user avatar
  • 123
0 votes
1 answer
248 views

Fine-grained complexity of 3-CNF formula evaluation

It's well known that 3-SAT is in NP, which means that one can evaluate a 3-CNF formula in polynomial time. However, I was wondering what the tightest upper bound is for formula verification, expressed ...
Joel Miller's user avatar