HW 1 : SAT Solver

[Manik Chugh]

Hi Brendon,

For the next homework, is it ok if we print the contents of the
required cnf file on the terminal, and then copy them to a file, save
the file and pass it to the SAT Solver.

Or do we need to write a file directly from PODEM.

I mean would the first method be fine or not?

-Manik

[Brendon Bolin]

Either is fine but I would figure most people would create a file directly since fprintf is not difficult to use.

--
______________________
Brendon Bolin
bbo...@gmail.com

[Adam Greenfield]

You could also use the '>' operator to redirect the output from the screen to a file and use that file as the input to the SAT solver.

EX: atpg C17.sim > C17.out

[Brendon Bolin]

Yes, you can redirect stdout to a file if you want. If you do so, you have to modify PODEM so it doesn't output its normal information on test pattern generation or you have to edit the files to remove that data. In my opinion, calling fopen, fprintf and fclose is simple and works fine.

You can also print everything to stderr and redirect that and you won't get the output from PODEM
ex: atpg C17.sim 2 > C17.out

Whatever you feel is easiest is fine.

[Manik Chugh]

Ok...few more things.

First, the homework pdf says download the software and go through the
readme file and the tutorial....I have not been able to find the
mentioned tutorial on the website....Can somebody please give me a
link for the same.

Secondly, I have made the C code in PODEM package which generates the
cnf file for the entered circuit....running the file with zchaff
package as : "./zchaff C17.cnf" returns some results like event is
satisfiable and some statistics, but it doesnt say anything about '0
justifiable' or '1 justifiable'. Also, the pdf asks us to provide the
equation that will make the output SAT for the circuits which are SAT.
I am not getting exactly what we need to do....Perhaps due to the
missing tutorial.

Lastly, in the portion PROGRAMING ASSIGNMENT of the pdf, it says in
the hint part: "First make that CNF for the entire circuit, and then
worry about testing the individual outputs. Each output can be tested
individually by added an additional clause that contains only the
desired output. This should make your program much simpler". I didnt
get this as well.

- Manik

On Feb 19, 4:33 pm, Brendon Bolin <bbo...@gmail.com> wrote:
> Yes, you can redirect stdout to a file if you want. If you do so, you have
> to modify PODEM so it doesn't output its normal information on test pattern
> generation or you have to edit the files to remove that data. In my opinion,
> calling fopen, fprintf and fclose is simple and works fine.
>
> You can also print everything to stderr and redirect that and you won't get
> the output from PODEM
> ex: atpg C17.sim 2 > C17.out
>
> Whatever you feel is easiest is fine.
>
> On Fri, Feb 19, 2010 at 4:24 PM, Adam Greenfield <
>
>
>
> aggreenfi...@umail.ucsb.edu> wrote:
> > You could also use the '>' operator to redirect the output from the screen
> > to a file and use that file as the input to the SAT solver.
>
> > EX: atpg C17.sim > C17.out
>
> > On Fri, Feb 19, 2010 at 11:18 AM, Brendon Bolin <bbo...@gmail.com> wrote:
>
> >> Either is fine but I would figure most people would create a file directly
> >> since fprintf is not difficult to use.
>

[Brendon Bolin]

First,
http://www.princeton.edu/~jdonald/research/zchaff/How%20to%20Use%20Chaff.ppt

Second,
You create the appropriate CNF clauses so the SAT solver will find if the output can be 0 or 1.

Third,
The suggestion is so you can create one CNF file instead of one per PO.

[Adam Greenfield]

What method should we go about including clauses for each output?

Are we checking for the whole circuit to be SAT, or individual outputs?? (for instance, one circuit only had 2 outputs that were satisfiable).

With the one output file, should we include a clause for each output being being 1?

[Brendon Bolin]

You can just add clauses to the file at the bottom and update the number of clauses.

You are checking individual outputs which will tell you if the circuit is SAT as well.

If you are including a clause for the output being 1 you are seeing if the output is 1 justifiable.

Brendon

[Adam Greenfield]

If I add all the clauses for each output at the end of the circuit,
zchaff will check the circuit as a whole for satisfiability.

(for example adding
11 0
10 0
to the output of C17.sim).

Does it make sense to create an output file for each output, adding
the output clause in each one? I can see no other way to distinguish
between individual outputs when running the CNF equations through
zchaff

On Feb 24, 11:58 am, Brendon Bolin <bbo...@gmail.com> wrote:
> You can just add clauses to the file at the bottom and update the number of
> clauses.
>
> You are checking individual outputs which will tell you if the circuit is
> SAT as well.
>
> If you are including a clause for the output being 1 you are seeing if the
> output is 1 justifiable.
>
> Brendon
>
> On Wed, Feb 24, 2010 at 11:54 AM, Adam Greenfield <
>
>
>
> aggreenfi...@umail.ucsb.edu> wrote:
> > What method should we go about including clauses for each output?
>
> > Are we checking for the whole circuit to be SAT, or individual outputs??
> > (for instance, one circuit only had 2 outputs that were satisfiable).
>
> > With the one output file, should we include a clause for each output being
> > being 1?
>
> > On Sat, Feb 20, 2010 at 12:44 PM, Brendon Bolin <bbo...@gmail.com> wrote:
>
> >> First,
>

> >>http://www.princeton.edu/~jdonald/research/zchaff/How%20to%20Use%20Ch...<http://www.princeton.edu/%7Ejdonald/research/zchaff/How%20to%20Use%20...>

>
> >> Second,
> >> You create the appropriate CNF clauses so the SAT solver will find if the
> >> output can be 0 or 1.
>
> >> Third,
> >> The suggestion is so you can create one CNF file instead of one per PO.
>

[Brendon Bolin]

If you don't add anything it will check the whole circuit for satisfiability. If you add one clause at a time you can check for 1 or 0 justifiability for that output.

You can create multiple output files if you want.

[Greg]

Hi Brendon,

A few questions about the report:

1. "You should include whether each circuit was SAT or UN-SAT".
To do this, we check if both 0 and 1 justifiable, and if both are SAT,
the circuit is SAT [at that output]?
And if we find that it is SAT at all [tested] outputs, the circuit is
considered SAT overall?

2. "If it was SAT, then provide the equation that will make each
output SAT."
Can you elaborate on this please? I'm not sure I understand this
request.

Thanks for your help; much appreciated!
- Gregory

On Feb 24, 12:29 pm, Brendon Bolin <bbo...@gmail.com> wrote:
> If you don't add anything it will check the whole circuit for
> satisfiability. If you add one clause at a time you can check for 1 or 0
> justifiability for that output.
>
> You can create multiple output files if you want.
>

> >http://www.princeton.edu/~jdonald/research/zchaff/How%20to%20Use%20Ch..<http://www.princeton.edu/%7Ejdonald/research/zchaff/How%20to%20Use%20Ch..>
> > .<http://www.princeton.edu/%7Ejdonald/research/zchaff/How%20to%20Use%20..