Linked Questions

1
vote
0answers
53 views

Start using SAT Solvers [duplicate]

What i actually want to do is to turn a math problem ,i have to solve,to a Boolean Satisfiability problem and solve it using a SAT Solver. I wonder if someone knows any manual,guide or anything that ...
18
votes
3answers
737 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,...
6
votes
2answers
538 views

Modeling the problem of finding all stable sets of an argumentation framework as SAT

As a continuation of my previous question i will try to explain my problem and how i am trying to convert my algorithm to a problem that can be expressed in a CNF form. Problem: Find all stable sets ...
3
votes
2answers
617 views

Mapping graph to another graph's sub-graph

How to solve the induced sub-graph isomorphism problem?
4
votes
1answer
406 views

transformation of constraint satisfaction to SAT

How can any Constraint satisfaction problem be converted to an instance of Satisfiability? I have a CSP and i know its NP hard to solve it, but i would like to convert to an instance of k-SAT, but im ...
4
votes
1answer
1k views

Algorithms for solving Flow game

Lately I've been toying with an automatic solver for the Android/iPhone game Flow. In this game, you start with several pairs of squares on a grid, and you have to connect each pair, without crossing ...
1
vote
1answer
151 views

Requiring at least one alldiff constraint to be satisfied converted to SAT

For generating certain hard puzzles, I am trying to model a problem (ultimately) in SAT. I don't know how to do that, so I am starting with CSP because it's more expressive. In CSP, there is a global ...
4
votes
1answer
114 views

Placing 1d items in a 2d grid with constraints

I'M looking for an algorithm (preferably polynomial) for the following problem: Input: - an M x N grid, where each square can be either empty or occupied - a list of items - a list of constraints ...
1
vote
1answer
141 views

Covering grid with constrained rectangles

I need to place N rects on a 2-dimensional grid with constraints. For the each rect height/width and placing limitations($x_{min}$-$x_{max}$) are known. The problem is to place all rects on a grid ...
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 ...
1
vote
1answer
37 views

How to express a structure of a 5-colorable graph in logic

A graph can be expressed as an structure $G = <A,R>$ satisfying the axioms $ \forall xy R(x,y) \rightarrow R(y,x)$ and $ \forall x \lnot R(x,x)$. How to extend the structure and/or axioms to ...