Re: MINISAT INCREMENTAL MODE STEP BY STEP GUIDE

[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

On 15/05/18 19:09, Ravi Kuril wrote:

looks like nobody want to help

On Monday, May 7, 2018 at 3:27:48 PM UTC+5:30, Ravi Kuril wrote:

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.

--

---
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.

[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

On 15 May 2018, at 14:13, Ravi Kuril <ravik...@gmail.com> wrote:

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.

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

[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

On 15 May 2018, at 20:16, Ravi Kuril <ravik...@gmail.com> wrote:

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