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 ...
533 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,...
464 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 ...
486 views

Mapping graph to another graph's sub-graph

How to solve the induced sub-graph isomorphism problem?
766 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 ...
243 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 ...
140 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 ...
134 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 ...
112 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 ...
35 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 ...