Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Default setting for variables #705

Open
Shikhar-Srivastava-16 opened this issue Mar 8, 2025 · 2 comments
Open

Default setting for variables #705

Shikhar-Srivastava-16 opened this issue Mar 8, 2025 · 2 comments
Assignees
Labels
area::sat Related to SAT rules, SAT solvers and the KisSAT solver interface.

Comments

@Shikhar-Srivastava-16
Copy link
Contributor

rustsat's native variable management generates solutions to decision variables in a Ternary format:

pub enum TernaryVal {
    True = 0,
    False = 1,
    DontCare = 2,
}

The conversion to binary supports default settings for variables which do not affect the satisfiablility of the expression given to it.
At the moment, I have this set to false as a placeholder.

There are a few ways this can be dealt with, including but perhaps not limited to:

  1. Treat this as a set default value - either false or true
  2. Treat this as a command line flag which allows us to set this value at runtime
  3. Just treat the solutions as Ternary, not Binary

I am unsure of how I can do this and I would like some advice.
Thanks

@Shikhar-Srivastava-16 Shikhar-Srivastava-16 added the area::sat Related to SAT rules, SAT solvers and the KisSAT solver interface. label Mar 8, 2025
@Shikhar-Srivastava-16 Shikhar-Srivastava-16 self-assigned this Mar 8, 2025
@niklasdewally
Copy link
Collaborator

See my comment here: #704 (comment)

@niklasdewally
Copy link
Collaborator

niklasdewally commented Mar 8, 2025

  • Treat this as a set default value - either false or true

This will change the number of solutions, which may break integration testing against Conjure.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area::sat Related to SAT rules, SAT solvers and the KisSAT solver interface.
Projects
None yet
Development

No branches or pull requests

2 participants