Questions tagged [sat-solvers]
Questions regarding solver programs for the boolean satisfiability problem.
77
questions
4
votes
2answers
101 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
22 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 ...
2
votes
1answer
63 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
30 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
609 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
48 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
34 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
38 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
70 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 ...
0
votes
0answers
35 views
How to apply AC-3(Arc-consistency 3) algorithm in N-Queen problem?
I am building N-Queen Solver with java.
I confused with AC-3 algorithm.
I heard that AC-3 can be applied with backtracking algorithm before processing and during the search.The latter is called MAC-3 ...
4
votes
0answers
37 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
34 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
49 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
52 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
153 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
155 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
114 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
327 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
159 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
157 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
48 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
89 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
115 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
142 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
139 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
823 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
116 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
111 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
409 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
1k 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
405 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
914 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
94 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
323 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 ...
18
votes
1answer
454 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
119 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
592 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
204 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
233 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
192 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
121 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
461 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
124 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
1k 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
160 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
926 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
47 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 ...
6
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 ...
