Questions tagged [sat-solvers]
Questions regarding solver programs for the boolean satisfiability problem.
105
questions
0
votes
1
answer
25
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?
CommunityBot
- 1
0
votes
1
answer
22
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).
...
- 11
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
0
votes
0
answers
8
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: \{\...
- 101
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
1
answer
81
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 ...
CommunityBot
- 1
1
vote
4
answers
2k
views
Is this possible to solve 3SAT in O(n^24) time and O(1) space?
Assume that n is the number variables of the given 3CNF formula (n≥3) and all clauses in the given 3CNF formula are different.
That means that for each clause, each literal can be either positive ...
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?
- 71
-1
votes
1
answer
43
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 ...
CommunityBot
- 1
0
votes
1
answer
208
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(...
CommunityBot
- 1
0
votes
0
answers
36
views
resolving in CDCL
When resolving in Conflict driven clause learning, it is the case that if you resolve a conflicting clause with the reason of the negation of one of his literals, then this results in another ...
- 55
1
vote
2
answers
71
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$ ...
D.W.♦
- 152k
1
vote
1
answer
112
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 ...
- 248
19
votes
3
answers
966
views
Recipe book for SAT encodings?
SAT solvers are getting more and more efficient in solving large instances and are being used as back-ends in various contexts.
Every time one wants to use them to solve a problem in a specific domain,...
CommunityBot
- 1
1
vote
1
answer
61
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 ...
- 26.5k
4
votes
1
answer
324
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 ...
- 268
2
votes
0
answers
51
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
1
answer
59
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 ...
D.W.♦
- 152k
3
votes
1
answer
60
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 ...
- 78
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
6
votes
1
answer
125
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 ...
- 8,013
2
votes
2
answers
554
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 ...
- 151
1
vote
1
answer
69
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 ...
- 274k
6
votes
3
answers
299
views
Detection of redundant boolean constraints
I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin ...
- 8,013
0
votes
0
answers
34
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 ...
- 229
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
1
answer
141
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$?
- 274k
11
votes
1
answer
846
views
Can top SAT-solvers factor easy numbers?
Modern SAT-solvers are very good at solving many real-world examples of SAT instances. However, we know how to generate hard ones: for instance use a reduction from factoring to SAT and give the RSA ...
- 8,013
1
vote
0
answers
61
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
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 ...
- 232
32
votes
3
answers
6k
views
Encoding 1-out-of-n constraint for SAT solvers
I'm using a SAT solver to encode a problem, and as part of the SAT instance, I have boolean variables $x_1,x_2,\dots,x_n$ where it is intended that exactly one of these should be true and the rest ...
- 186
1
vote
2
answers
317
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 ...
1
vote
1
answer
633
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 ...
- 6,777
3
votes
1
answer
48
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 ...
D.W.♦
- 152k
0
votes
2
answers
361
views
Constrain certain variables in CNF to unique satisfying assignments
[Reposted because the original question was deleted by the poster.]
I'm looking for a way to add additional clauses (and maybe additional variables) to an already existing SAT instance so that ...
- 11
2
votes
1
answer
538
views
How to choose between UC and PL when using the DPLL algorithm?
We know DPLL algorithm is backtracking + unit propagation + pure
literal rule.
I have an example. There is one example to solve following Satisfiability problem with DPLL. if assign of "0" to ...
- 8,013
3
votes
1
answer
108
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 ...
CommunityBot
- 1
4
votes
2
answers
387
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,...
- 559
3
votes
1
answer
136
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 ...
- 955
3
votes
1
answer
558
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 (...
- 13.1k
2
votes
1
answer
109
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 ...
- 274k
7
votes
1
answer
823
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.
...
- 81.1k
1
vote
1
answer
103
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'...
D.W.♦
- 152k
3
votes
1
answer
266
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 ...
- 12.5k
3
votes
2
answers
2k
views
CSP Forward checking with n-ary (and binary) constraints
I have implemented my own CSP solver using a Backtracking algorithm.
Within the Backtracking algorithm I apply a Forward Checking algorithm (reducing domains of connected, unnasigned variables) that ...
- 43
0
votes
1
answer
117
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 ...
- 12.5k
3
votes
0
answers
222
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
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
2
votes
1
answer
46
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 ...
- 274k
0
votes
1
answer
193
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 ...
- 81.1k