MINISAT INCREMENTAL MODE STEP BY STEP GUIDE

[Ravi kumar kuril]

HI,
Everyone my name is ravi kuril I am doing a thesis on SAT planning for my work i want to use incremental mode of the MINISAT tool.I am new to the Incremental approach of the tool. I just want to implement it i have clauses of a encoded problem but i don't know how to use minisat for incremental approach.A step by step guide would be really great favour. I am really short on time. Please reply.

[Ravi Kuril]

looks like nobody want to help

[Mate Soos]

Please read the old group discussions and read the documentation. Also, I strongly suggest you don't use all-capitals subject lines, it's considered rude and you are asking for a favor -- please be considerate.

Mate

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Ravi Kuril]

Hi i used it to indicate the time constraints. and i have gone through the documentation but could not find the basic steps for incremental approach. Neither i found the documentation from the minisat website. and its been tool long i could not get a single reply form anyone for help.

To unsubscribe from this group and stop receiving emails from it, send an email to minisat+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.

To unsubscribe from this group and stop receiving emails from it, send an email to minisat+unsubscribe@googlegroups.com.

[Michael Tautschnig]

You are more likely to receive help if you make it easy for others to help you. For example, you might send pseudo code that makes clear the inputs you provide and the output that you expect. In between you will add clauses and call the solve method.

Best,

Michael

To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.

[Ravi Kuril]

Hi michael i am glad you asked. I am trying to solve a puzzle in the sequential manner of time points. so in each time point i am adding new clauses into the the existed set of clauses  then again i am calling sat solver as a black box. So the execution is some thing like in each iteration whole set of clauses are solved by a fresh invocation of MINISAT solver.

So what i want is to make this sat solver keep alive for next set of clauses so that it can save solving time because it has learned  solutions of the some of the old set of clauses.

But the problem is i dont know what are the command set used by MINISAT to make it learn the clauses so that it can use them.

Thats why i asked if anyone who has implemented INCREMENTAL approach using MINISAT can solve tons of my problems.

If anyone knows INCREMENTAL approach in implementation point of view using MINISAT please help me.

Thanks in advance    

[Michael Tautschnig]

You might want to post your code for doing a single (non-incremental) run of the solver. With MiniSat’s API it’s not all that different and people will guide you properly.

Best,

Michael

To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.

[Ravi Kuril]

Hi, People apologies for late reply. I am attaching my code. In which i am trying to solve sokoban problem using SAT approach . build instruction can be found in README.md file.

As it can be seen i am calling SAT caller in each interation. I want to keep the sat solver alive so that it can learn clauses. curious fellow please have a look It wont take much of time of yours. Please ping me if anyone successfully implements the INCREMENTAL approach.

LINK:    https://drive.google.com/drive/folders/1Oi86lUeXU7du58tmbLtsmmJ5WfYXThbE?usp=sharing

Thanks In advance

Regrads

Ravi Kuril