Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

Filter by
Sorted by
Tagged with
1 vote
0 answers
49 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
34 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
  • 21
1 vote
1 answer
84 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
66 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,652
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
16 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
44 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,184
0 votes
1 answer
31 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
46 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
0 votes
0 answers
10 views

Do you resolve all clauses in the processed bucket in the Davis-Putnam algorithm?

I'm reading the description and example of Davis-Putnam on page 102 of the Handbook of Satisfiability and I'm confused by the example they use. To start with, they fill the following buckets $C: \{\...
azani's user avatar
  • 101
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 $...
vvg's user avatar
  • 135
-1 votes
1 answer
46 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
  • 305
2 votes
2 answers
93 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
  • 305
0 votes
1 answer
298 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
176 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
62 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
473 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
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 ...
Geremia's user avatar
  • 142
2 votes
1 answer
94 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
69 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
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 ...
Dan D-man's user avatar
  • 494
6 votes
1 answer
148 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
98 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,881
0 votes
0 answers
52 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
146 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
148 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
61 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
398 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
49 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
92 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
759 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
123 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
434 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,...
faceclean's user avatar
  • 568
3 votes
1 answer
170 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
738 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
120 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
854 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
142 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
313 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
122 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
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 ...
Gabe Burke's user avatar
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 ...
Alex's user avatar
  • 263
2 votes
1 answer
47 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
223 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
1 vote
1 answer
87 views

Why not do these checks on the number of clauses in 3-SAT?

I've been writing a 3-SAT solver for fun and comparing its performance against the solver pycosat. My solver vastly outperforms pycosat in two special cases, where I solve by doing simple, obvious ...
Rachel's user avatar
  • 113
3 votes
1 answer
342 views

Detect non existence of a cycle in a graph using Datalog : SMTLIB Format for Z3

I want to detect the non existence of a cycle in a graph using Datalog (which is a declarative logic programming language). The proposed solution was: ...
Josep Ng's user avatar
2 votes
2 answers
642 views

Is any sudoku solver an SAT solver?

I have recently created a sudoku solver using C#, which outputs the solution to a sudoku after a reasonable amount of time in many cases. I have used the basic sudoku SAT-reduction (i.e. x111 meaning ...
Schmetterling's user avatar
1 vote
0 answers
169 views

General Understanding of SMT Solving Across Multiple Theories

My first question was a little too simplified in that it turned out to be an integer linear programming problem solvable with the Simplex Method. However, what I think I am wondering about is how to ...
Lance's user avatar
  • 2,163