Questions tagged [sat-solvers]
Questions regarding solver programs for the boolean satisfiability problem.
87
questions
0
votes
0answers
11 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 ...
1
vote
0answers
83 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 ...
1
vote
1answer
18 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$?
1
vote
0answers
51 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 ...
2
votes
1answer
42 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 ...
1
vote
2answers
101 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
1answer
35 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 ...
11
votes
3answers
2k views
Are there competitions for integer programming?
Are there competitions for integer programming like there are for SAT and MAXSAT?
2
votes
1answer
47 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 ...
1
vote
1answer
114 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 ...
3
votes
1answer
72 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 ...
4
votes
2answers
213 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,...
3
votes
1answer
52 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 ...
3
votes
1answer
184 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 (...
2
votes
1answer
50 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 ...
7
votes
1answer
687 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.
...
1
vote
1answer
63 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'...
3
votes
1answer
120 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 ...
0
votes
1answer
74 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 ...
3
votes
0answers
122 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 ...
4
votes
0answers
50 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 ...
2
votes
1answer
40 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 ...
0
votes
1answer
92 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 ...
1
vote
1answer
62 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 ...
3
votes
1answer
214 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:
...
1
vote
1answer
289 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 ...
1
vote
0answers
133 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 ...
3
votes
1answer
481 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 ...
-2
votes
1answer
226 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
vote
1answer
197 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)$, ...
0
votes
1answer
55 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 ...
3
votes
0answers
105 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 ...
0
votes
1answer
217 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
1answer
165 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?
2
votes
1answer
197 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 ...
2
votes
1answer
1k 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 ...
0
votes
0answers
138 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 ...
0
votes
1answer
131 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
vote
1answer
773 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
2answers
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 ...
1
vote
1answer
527 views
Is this possible to solve 4SAT in polynomial time? [closed]
I know and admit that this is long, but please read it slow and understand everything.
I think that this is one of the most interesting questions asked in computer science ever.
I don't expect for ...
1
vote
4answers
1k 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 ...
0
votes
0answers
107 views
These sample CNF formulas in DIMACS files are in P? (Schaefer's dichotomy theorem)
Here is my earlier question. But there was no full answer.
I've decided to include specific DIMACS files:
http://jarvis2.hmcloud.pl/sat/cnf.formula.10 (15.8MB)
http://jarvis2.hmcloud.pl/sat/cnf....
3
votes
1answer
434 views
What's the average number of clauses modern SAT solvers can handle?
It's already known that size doesn't matter always (for SAT problems).
But is there evidence (from real data from: benchmarks or real cases) on how many clauses an average SAT solver can handle ...
19
votes
1answer
593 views
Why do all recent SAT solvers work on CNF instead of circuit SAT?
After the release of the AIGER library to handle and-inverter graphs sometime in 2006 (I think), some circuit SAT solvers were released in 2006-2008, and in a few SAT Races/Competitions there were AIG ...
1
vote
0answers
124 views
Logical formula in DIMACS, SAT, Schaefer's dichotomy theorem and software to test it
I have a very complicated formula logical (CNF) in the file DIMACS.
The question is as follows. The formula has hundreds of millions of clauses (assume billion) and a lot of variables.
It is a ...
8
votes
4answers
677 views
Deterministic SAT solver
I have the following question. Is the SAT solvers are deterministic?
I mean, for example, about miniSAT and DPLL algorithm. Are they completely deterministic?
If these algorithms will return unSAT ...
7
votes
1answer
1k views
Why the need for TSP solvers when there are SAT solvers?
Concorde TSP is a solver for TSP. SAT solvers are solvers for boolean satisfiability. TSP and SAT are NP-complete.
Hence, why spent the time to develop Concorde TSP when there is an abundance of SAT ...
1
vote
2answers
1k views
Best improvements to do to the DPLL SAT algorithm
As part of a college class, I'm asked to improve the performance of a basic DPLL sat solver. I'm already provided a basic, slow working version (essentially the DPLL algorithm; furthermore, to select ...
6
votes
1answer
232 views
Framework or tools to generate theorem prover/solver/reasoner for new logic
I have new logic which has syntax and semantics in usual natural languages and I have to create theorem prover/solver/reasoner for this logic. Is there framework or tool set that can generate such ...
