Questions tagged [sat-solvers]
Questions regarding solver programs for the boolean satisfiability problem.
3
votes
0answers
23 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
29 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
34 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
46 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
108 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
97 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
72 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
174 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
67 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
126 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
42 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
81 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
79 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 ...
2
votes
1answer
93 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?
1
vote
1answer
110 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
527 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-...
0
votes
0answers
85 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
108 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 ...
0
votes
1answer
284 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
1answer
840 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
309 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 ...
0
votes
2answers
577 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
62 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
273 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 ...
17
votes
1answer
353 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
108 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
529 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
811 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
867 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 ...
5
votes
1answer
185 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 ...
1
vote
1answer
189 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 ...
7
votes
1answer
185 views
How to use an old SAT solver to discover a new one, as is done in The Golden Ticket?
In Lance Fortnow's book The Golden Ticket, he mentions that once you have a polynomial-time algorithm for an NP-complete problem, you can use it to find a faster algorithm. Can you tell me how that is ...
1
vote
1answer
107 views
Using SMT Solvers in formula checking
I'm currently working on a static analysis work in which I need to check whether a given formula is met or not. I hope the following example clarifies my requirement.
Suppose we have a list of three-...
3
votes
4answers
401 views
How to Modify SAT Solvers to Produce Resolution Refutations for Unsatisfiable Instances?
In recent SAT competitions, there is a Certified UNSAT track. The problem instances are all unsatisfiable and the solvers are asked to produce certificates for unsatisfiability. One way is to produce ...
1
vote
1answer
91 views
Does MiniSAT need exponential time?
I'm asking for a sequence of instances for SAT, one instance for each length, such that the sequence takes exponential time with MiniSAT.
7
votes
1answer
922 views
Why is pure literal elimination absent in DPLL-based algorithms like Chaff?
I'm looking into various SAT-solvers and trying to understand how they work and why they are designed in certain ways. (But I'm not in a university at the moment and I do not know anyone who is a ...
8
votes
2answers
152 views
Assignment to make formula unsatisfiable
Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?". One way of ...
9
votes
1answer
861 views
Conflict Driven Clause Learning backtracking clarification
On the wikipedia page here it describes pretty well the CDCL algorithm (and it seems the pictures were taken from slides created by Sharad Malik at Princeton). However when describing how to backtrack ...
1
vote
0answers
38 views
A query regarding the Max3SAT Approximation Algorithm's Application
Its known that a polynomial time Approximation Algorithm that satisfies 3MaxSAT in 7/8+e clauses implies P=NP. If given that the given 3MaxSAT is satisfiable, it is still difficult to find a 7/8+e ...
5
votes
2answers
1k views
Why don't modern SAT solvers use the notion of a “watched clause”, in the same way they use the notion of a “watched literal”?
Modern SAT solvers use the notion of "watched literals": when a value is chosen for a literal $l$, the solver only checks whether that falsifies clauses with $l$ in them if $l$ is one of the watched ...
2
votes
1answer
377 views
Basic question about backjumping in SAT solvers
I am reading "Formalization and Implementation of Modern SAT Solvers", by Filip Marić.
My question is about how backjumping is defined. In an example [1], there is a conflict clause C equal to
[-1,-...
4
votes
2answers
839 views
Are there any open source SAT solvers with UNSAT core extraction algorithm built in?
Just like the title says. I need to use a SAT solver on a series of CNF formulas but not only do I need an answer of the type satisfiable/unsatisfiable but also some subset of clauses whose ...
1
vote
1answer
127 views
How is the complexity of algorithms to solve 3CNF (decision problem) specified? [duplicate]
For k inputs, the complexity of naive algorithm is O(2^k). I understood this one.
What is meant by "the size of the instance to be solved should be polynomial in k". Is it equivalent to the statement ...
1
vote
1answer
141 views
SAT for arithmetic
Given two integers $X$ and $Y$, each can be encoded in binary $X=(x_4 x_3 x_2 x_1)$ and $Y=(y_4 y_3 y_2 y_1)$, how do I encode each one of the constraints
$$|X-Y|\geq n \quad\text{and}\quad|X-Y|= n$$...
7
votes
2answers
122 views
Common method for solving satisfiability problems which lie in P
I know from Schaefer's Dichotomy Theorem that only a few types of satisfiability problems are in P and any other problem is NP-complete. However, all of the algorithms I know for them use specific ...
0
votes
2answers
197 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 ...
2
votes
1answer
42 views
SMT solves with functions for free varibles
So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions ...
5
votes
1answer
299 views
Why is DPLL better than brute force?
I understand that by being clever about the way we navigate the search space of the SAT problem we're going to get better performance than by randomly choosing and testing solutions, though of course ...
2
votes
1answer
91 views
Sound and complete algorithms for boolean satifiability
To my best knowledge, these are the sound and complete algorithms for boolean satisfiability
Variations of DPLL algorithm (e.g. CDCL, Look-ahead solvers)
Stalmarks method
Binary Decision Diagram (BDD)...
15
votes
3answers
463 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,...
