10 questions linked to/from Converting (math) problems to SAT instances
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 ...
579 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,...
471 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 ...
499 views

### Mapping graph to another graph's sub-graph

How to solve the induced sub-graph isomorphism problem?
805 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 ...
255 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 ...
141 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 ...
137 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 ...
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 ...