Questions tagged [sat-solvers]
Questions regarding solver programs for the boolean satisfiability problem.
97
questions
1
vote
1
answer
40
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 ...
- 23
0
votes
0
answers
15
views
How overapproximation of boolean abstraction function works?
I just found that if original formula is unsat, using boolean abstraction function can result in sat. Clearly this is overapproximate. I wonder if I have contingent formula, does that means my boolean ...
4
votes
1
answer
68
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 ...
- 43
2
votes
0
answers
28
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 ...
- 145
2
votes
1
answer
33
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 ...
- 199
3
votes
1
answer
42
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 ...
- 53
2
votes
0
answers
33
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 ...
6
votes
1
answer
84
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 ...
- 161
0
votes
0
answers
14
views
Getting maximum information regarding question key from students answers
You are given a multi-dimensional array with each index consisting of two attributes (Score, Answers)
Each element in the array represents the test results of a student on a True or False exam. Each ...
- 15
1
vote
1
answer
32
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 ...
- 2,820
0
votes
0
answers
23
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 ...
- 219
1
vote
0
answers
121
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
52
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$?
- 13
1
vote
0
answers
55
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
52
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 ...
- 359
1
vote
2
answers
210
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 ...
3
votes
1
answer
43
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 ...
- 213
11
votes
3
answers
2k
views
Are there competitions for integer programming?
Are there competitions for integer programming like there are for SAT and MAXSAT?
- 294
2
votes
1
answer
69
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 ...
- 21
0
votes
1
answer
316
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 ...
- 174
3
votes
1
answer
91
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 ...
- 677
4
votes
2
answers
311
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,...
- 549
3
votes
1
answer
65
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 ...
- 131
3
votes
1
answer
318
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 (...
- 33
2
votes
1
answer
70
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 ...
- 375
7
votes
1
answer
765
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.
...
- 386
1
vote
1
answer
77
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'...
- 583
3
votes
1
answer
187
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 ...
- 209
0
votes
1
answer
96
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 ...
- 183
3
votes
0
answers
171
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
59
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 ...
- 243
2
votes
1
answer
42
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 ...
- 123
0
votes
1
answer
139
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 ...
- 149
1
vote
1
answer
74
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 ...
- 113
3
votes
1
answer
281
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:
...
- 31
2
votes
2
answers
406
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 ...
- 103
1
vote
0
answers
146
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 ...
- 1,853
3
votes
1
answer
533
views
How the Abstract DPLL Algorithm Works in SAT Solving
I have come across many definitions of the DPLL algorithm but haven't been able to follow them. The ones that are closest to making sense to me are the ones based on state-transition systems with ...
- 1,853
-2
votes
1
answer
250
views
How a SMT / SAT Solver Generates Valuations for this Example
First, an example of a set of constraints which turned out not to be solvable (I don't think):
...
- 1,853
1
vote
1
answer
242
views
Counting solutions of a particular type in HORN SAT
I am interested in counting the number of solutions of a particular type (say #) in HORN SAT. I have 2 questions concerning the same.
Suppose we have a HORN SAT -: $(x_1) \land (x_2 \implies x_1)$, ...
- 321
0
votes
1
answer
67
views
How to find a nearly-optimal covering of a set using SAT?
I have recently started thinking about application of SAT in solving different problems and how I can encode those problems into a SAT problem.
I think one of the interesting problems where SAT ...
- 153
3
votes
0
answers
124
views
How hard is APPROXIMATE-#SAT? [closed]
It is well known that the problem of counting the satisfying assignments of SAT, namely the problem #SAT, is #P-complete.
It is also suspected (somewhat less widely) that even deciding SAT should ...
- 31
0
votes
1
answer
269
views
SAT solver optimizations of DPLL for unsatisfiable formulas [duplicate]
I am implementing a SAT solver based on DPLL algorithm, and it works fine on small formulas and larger satisfiable problems. My case split is based on a tree like structure, where every branch is ...
3
votes
1
answer
181
views
If a CNF contains only Horn and Xor clauses, then what is the complexity of determining Satisfiability?
If a CNF contains only Horn and Xor clauses, and does not contain clauses of other types, then can its Satisfiability be determined in polynomial time?
- 321
2
votes
1
answer
226
views
What is the complexity of determining Satisfiability of a CNF containing both Horn and Dual Horn clauses?
If a CNF contains both horn and dual horn clauses and does not contain clauses of other types, then can its Satisfiability always be determined in polynomial time?
If the answer to the above problem ...
- 321
2
votes
1
answer
2k
views
Bit Blasting Algorithm
I found a pseudo algorithm which describes bit blasting: click (page 156,157). I am trying to implement it in C, but I don't understand it yet completely. Let's make an example:
Assume our bit-vectors ...
- 637
0
votes
0
answers
151
views
When to use SAT vs solving?
Are there any guidelines for how to recognize, for a given problem, which approach is more likely to yield good results? SAT solver or SMT solver?
Is there any guidance anyone can offer about which ...
- 101
0
votes
1
answer
143
views
Another way to solve SAT. Was it known?
Theorem. If and only if SAT instance $\varphi$ is satisfiable, there is a way to negate variables in $\varphi$ and get $\varphi'$ where all clauses have at least one positive literal.
Also we can ...
- 1,371
1
vote
1
answer
1k
views
Is this possible to solve SAT in polynomial time by reducing it to the problem of solving system of nonlinear equations?
Every conjunctive normal form (CNF) formula can be converted to nonlinear system of equations, where each clause becomes an equation in the system and:
If A and B are logical/boolean variables and ...
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 ...
- 31