0

I'm modeling a problem with SAT and trying to solve it with cryptominisat. I'd like to give my variable a default value if there's no constraint for it.

I went through the manual and set_default_polarity seems like the answer. I tried it out but it doesn't work as I expected. I don't really get the term polarity here. Some googling didn't help me out as I'm not familiar with logic.

So, my questions are:

  1. Would you kindly explain what polarity is or point me to some introductory-level sources?

  2. Is there an interface in cryptominisat(or in SAT solvers generally) to set default value for logic variables? What is the term for such functionality?

Thanks.

1 Answer 1

0

cryptominisat --hhelp (note the extra h!) gives the following extended help:

.....
  --polar arg (=auto)                   {true,false,rnd,auto} Selects polarity
                                        mode. 'true' -> selects only positive
                                        polarity when branching. 'false' ->
                                        selects only negative polarity when
                                        brancing. 'auto' -> selects last
                                        polarity used (also called 'caching')
.....

I use --polar=false to let cryptominisat search for solutions with false/0 variables first, because my examples have most solution variables that way.

In the source, this corresponds to solverconf.h:

enum class PolarityMode {
    polarmode_pos
    , polarmode_neg
    , polarmode_rnd
    , polarmode_automatic
};

The respective SolverConf variable is PolarityMode polarity_mode

In main.cpp is shown how to set this configuration property in a program:

if (vm.count("polar")) {
        string mode = vm["polar"].as<string>();

        if (mode == "true") conf.polarity_mode = polarmode_pos;
        else if (mode == "false") conf.polarity_mode = polarmode_neg;
        else if (mode == "rnd") conf.polarity_mode = polarmode_rnd;
        else if (mode == "auto") conf.polarity_mode = polarmode_automatic;
        else throw WrongParam(mode, "unknown polarity-mode");
    }

Other SAT solvers are using terms like phase or sign.

Microsoft Z3 can be parameterized via commandline sat.phase=always_false to try false phase first. See a related question. Actually, my first question on StackOverflow back in 2012.

Clasp is using commandline syntax --sign-def=neg to take false polarity first.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.